The cat is big. The cat is rough. The cat needs the lion. The dog chases the cat. The dog chases the lion. The dog is big. The dog is cold. The dog is red. The lion chases the dog. The lion is cold. The lion likes the cat. The lion needs the cat. If the lion needs the cat and the cat likes the lion then the cat needs the dog. If the lion likes the cat then the cat likes the lion.
The cat is big.
("cat" "is" "big" "+")
The cat is rough.
("cat" "is" "rough" "+")
The cat needs the lion.
("cat" "needs" "lion" "+")
The dog chases the cat.
("dog" "chases" "cat" "+")
The dog chases the lion.
("dog" "chases" "lion" "+")
The dog is big.
("dog" "is" "big" "+")
The dog is cold.
("dog" "is" "cold" "+")
The dog is red.
("dog" "is" "red" "+")
The lion chases the dog.
("lion" "chases" "dog" "+")
The lion is cold.
("lion" "is" "cold" "+")
The lion likes the cat.
("lion" "likes" "cat" "+")
The lion needs the cat.
("lion" "needs" "cat" "+")
If the lion needs the cat and the cat likes the lion then the cat needs the dog.
((("lion" "needs" "cat" "+") ("cat" "likes" "lion" "+")) -> ("cat" "needs" "dog" "+"))
If the lion likes the cat then the cat likes the lion.
((("lion" "likes" "cat" "+")) -> ("cat" "likes" "lion" "+"))
The lion needs the cat.
True
1
proof
[(triple12)]
("lion" "needs" "cat" "+")
triple12
The lion does not chase the dog.
False
1
inv-proof
[(triple9)]
("lion" "chases" "dog" "-")
triple9
The cat likes the lion.
True
2
proof
[(((triple11) -> rule2))]
("cat" "likes" "lion" "+")
((triple11) -> (rule2 % int1))
The cat likes the lion.
("cat" "likes" "lion" "+")
int1
The cat does not like the lion.
False
2
inv-proof
[(((triple11) -> rule2))]
("cat" "likes" "lion" "-")
((triple11) -> (rule2 % int1))
The cat likes the lion.
("cat" "likes" "lion" "+")
int1
The cat needs the dog.
True
4
proof
[(((triple12 ((triple11) -> rule2)) -> rule1))]
("cat" "needs" "dog" "+")
((triple12 ((triple11) -> (rule2 % int2))) -> (rule1 % int1))
The cat needs the dog.
("cat" "needs" "dog" "+")
int1
The cat likes the lion.
("cat" "likes" "lion" "+")
int2
The cat does not need the dog.
False
4
inv-proof
[(((triple12 ((triple11) -> rule2)) -> rule1))]
("cat" "needs" "dog" "-")
((triple12 ((triple11) -> (rule2 % int2))) -> (rule1 % int1))
The cat needs the dog.
("cat" "needs" "dog" "+")
int1
The cat likes the lion.
("cat" "likes" "lion" "+")
int2
The lion does not like the dog.
Unknown
inv-random
[@0: The lion likes the dog.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "dog" "-")
The dog likes the cat.
Unknown
random
[@0: The dog likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "cat" "+")
The dog does not need the lion.
Unknown
inv-random
[@0: The dog needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "lion" "-")
The dog likes the dog.
Unknown
random
[@0: The dog likes the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "dog" "+")
The dog does not need the cat.
Unknown
inv-random
[@0: The dog needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "cat" "-")
The dog chases the dog.
Unknown
random
[@0: The dog chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "dog" "+")
@0: The cat is big.[(triple1)] The cat is rough.[(triple2)] The cat needs the lion.[(triple3)] The dog chases the cat.[(triple4)] The dog chases the lion.[(triple5)] The dog is big.[(triple6)] The dog is cold.[(triple7)] The dog is red.[(triple8)] The lion chases the dog.[(triple9)] The lion is cold.[(triple10)] The lion likes the cat.[(triple11)] The lion needs the cat.[(triple12)] @1: The cat likes the lion.[(((triple11) -> rule2))] @2: The cat needs the dog.[(((triple12 ((triple11) -> rule2)) -> rule1))]
The cat is big.
("cat" "is" "big" "+")
triple1
The cat is rough.
("cat" "is" "rough" "+")
triple2
The cat needs the lion.
("cat" "needs" "lion" "+")
triple3
The dog chases the cat.
("dog" "chases" "cat" "+")
triple4
The dog chases the lion.
("dog" "chases" "lion" "+")
triple5
The dog is big.
("dog" "is" "big" "+")
triple6
The dog is cold.
("dog" "is" "cold" "+")
triple7
The dog is red.
("dog" "is" "red" "+")
triple8
The lion chases the dog.
("lion" "chases" "dog" "+")
triple9
The lion is cold.
("lion" "is" "cold" "+")
triple10
The lion likes the cat.
("lion" "likes" "cat" "+")
triple11
The lion needs the cat.
("lion" "needs" "cat" "+")
triple12
The cat likes the lion.
("cat" "likes" "lion" "+")
((triple11) -> (rule2 % int1))
The cat likes the lion.
("cat" "likes" "lion" "+")
int1
The cat needs the dog.
("cat" "needs" "dog" "+")
((triple12 ((triple11) -> (rule2 % int2))) -> (rule1 % int1))
The cat needs the dog.
("cat" "needs" "dog" "+")
int1
The cat likes the lion.
("cat" "likes" "lion" "+")
int2