The cat eats the lion. The cat is kind. The cat needs the dog. The dog eats the cat. The dog eats the tiger. The dog likes the cat. The dog needs the cat. The lion eats the dog. The lion is kind. The lion is young. The lion likes the tiger. The tiger needs the cat. If something likes the tiger then it likes the lion. If something eats the dog and the dog is blue then the dog eats the cat. If something likes the cat then it likes the tiger.
The cat eats the lion.
("cat" "eats" "lion" "+")
The cat is kind.
("cat" "is" "kind" "+")
The cat needs the dog.
("cat" "needs" "dog" "+")
The dog eats the cat.
("dog" "eats" "cat" "+")
The dog eats the tiger.
("dog" "eats" "tiger" "+")
The dog likes the cat.
("dog" "likes" "cat" "+")
The dog needs the cat.
("dog" "needs" "cat" "+")
The lion eats the dog.
("lion" "eats" "dog" "+")
The lion is kind.
("lion" "is" "kind" "+")
The lion is young.
("lion" "is" "young" "+")
The lion likes the tiger.
("lion" "likes" "tiger" "+")
The tiger needs the cat.
("tiger" "needs" "cat" "+")
If something likes the tiger then it likes the lion.
((("something" "likes" "tiger" "+")) -> ("something" "likes" "lion" "+"))
If something eats the dog and the dog is blue then the dog eats the cat.
((("something" "eats" "dog" "+") ("dog" "is" "blue" "+")) -> ("dog" "eats" "cat" "+"))
If something likes the cat then it likes the tiger.
((("something" "likes" "cat" "+")) -> ("something" "likes" "tiger" "+"))
The dog eats the tiger.
True
1
proof
[(triple5)]
("dog" "eats" "tiger" "+")
triple5
The tiger does not need the cat.
False
1
inv-proof
[(triple12)]
("tiger" "needs" "cat" "-")
triple12
The lion likes the lion.
True
2
proof
[(((triple11) -> rule1))]
("lion" "likes" "lion" "+")
((triple11) -> (rule1 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1
The lion does not like the lion.
False
2
inv-proof
[(((triple11) -> rule1))]
("lion" "likes" "lion" "-")
((triple11) -> (rule1 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1
The dog likes the lion.
True
3
proof
[(((((triple6) -> rule3)) -> rule1))]
("dog" "likes" "lion" "+")
((((triple6) -> (rule3 % int2))) -> (rule1 % int1))
The dog likes the lion.
("dog" "likes" "lion" "+")
int1
The dog likes the tiger.
("dog" "likes" "tiger" "+")
int2
The dog does not like the lion.
False
3
inv-proof
[(((((triple6) -> rule3)) -> rule1))]
("dog" "likes" "lion" "-")
((((triple6) -> (rule3 % int2))) -> (rule1 % int1))
The dog likes the lion.
("dog" "likes" "lion" "+")
int1
The dog likes the tiger.
("dog" "likes" "tiger" "+")
int2
The tiger does not like the tiger.
Unknown
inv-rconc
[@1: The tiger likes the tiger.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("tiger" "likes" "tiger" "-")
The cat likes the tiger.
Unknown
rconc
[@1: The cat likes the tiger.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cat" "likes" "tiger" "+")
The cat does not like the lion.
Unknown
inv-rconc
[@2: The cat likes the lion.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("cat" "likes" "lion" "-")
The lion is rough.
Unknown
random
[@0: The lion is rough.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "rough" "+")
The cat does not eat the cat.
Unknown
inv-random
[@0: The cat eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "cat" "-")
The tiger eats the dog.
Unknown
random
[@0: The tiger eats the dog.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "dog" "+")
@0: The cat eats the lion.[(triple1)] The cat is kind.[(triple2)] The cat needs the dog.[(triple3)] The dog eats the cat.[(triple4)] The dog eats the tiger.[(triple5)] The dog likes the cat.[(triple6)] The dog needs the cat.[(triple7)] The lion eats the dog.[(triple8)] The lion is kind.[(triple9)] The lion is young.[(triple10)] The lion likes the tiger.[(triple11)] The tiger needs the cat.[(triple12)] @1: The dog likes the tiger.[(((triple6) -> rule3))] The lion likes the lion.[(((triple11) -> rule1))] @2: The dog likes the lion.[(((((triple6) -> rule3)) -> rule1))]
The cat eats the lion.
("cat" "eats" "lion" "+")
triple1
The cat is kind.
("cat" "is" "kind" "+")
triple2
The cat needs the dog.
("cat" "needs" "dog" "+")
triple3
The dog eats the cat.
("dog" "eats" "cat" "+")
triple4
The dog eats the tiger.
("dog" "eats" "tiger" "+")
triple5
The dog likes the cat.
("dog" "likes" "cat" "+")
triple6
The dog needs the cat.
("dog" "needs" "cat" "+")
triple7
The lion eats the dog.
("lion" "eats" "dog" "+")
triple8
The lion is kind.
("lion" "is" "kind" "+")
triple9
The lion is young.
("lion" "is" "young" "+")
triple10
The lion likes the tiger.
("lion" "likes" "tiger" "+")
triple11
The tiger needs the cat.
("tiger" "needs" "cat" "+")
triple12
The dog likes the tiger.
("dog" "likes" "tiger" "+")
((triple6) -> (rule3 % int1))
The dog likes the tiger.
("dog" "likes" "tiger" "+")
int1
The lion likes the lion.
("lion" "likes" "lion" "+")
((triple11) -> (rule1 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1
The dog likes the lion.
("dog" "likes" "lion" "+")
((((triple6) -> (rule3 % int2))) -> (rule1 % int1))
The dog likes the lion.
("dog" "likes" "lion" "+")
int1
The dog likes the tiger.
("dog" "likes" "tiger" "+")
int2