The cat eats the tiger. The cat is big. The cat is blue. The cat is nice. The cat is not young. The cat likes the tiger. The cat needs the lion. The lion eats the tiger. The lion is not big. The lion likes the cat. The lion likes the tiger. The lion needs the cat. The lion needs the tiger. The tiger is nice. The tiger does not need the cat. If something likes the tiger and it is not nice then it does not need the tiger. Blue things are not young. If something needs the cat and the cat is nice then it likes the lion.
The cat eats the tiger.
("cat" "eats" "tiger" "+")
The cat is big.
("cat" "is" "big" "+")
The cat is blue.
("cat" "is" "blue" "+")
The cat is nice.
("cat" "is" "nice" "+")
The cat is not young.
("cat" "is" "young" "-")
The cat likes the tiger.
("cat" "likes" "tiger" "+")
The cat needs the lion.
("cat" "needs" "lion" "+")
The lion eats the tiger.
("lion" "eats" "tiger" "+")
The lion is not big.
("lion" "is" "big" "-")
The lion likes the cat.
("lion" "likes" "cat" "+")
The lion likes the tiger.
("lion" "likes" "tiger" "+")
The lion needs the cat.
("lion" "needs" "cat" "+")
The lion needs the tiger.
("lion" "needs" "tiger" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
The tiger does not need the cat.
("tiger" "needs" "cat" "-")
If something likes the tiger and it is not nice then it does not need the tiger.
((("something" "likes" "tiger" "+") ("something" "is" "nice" "~")) -> ("something" "needs" "tiger" "-"))
Blue things are not young.
((("something" "is" "blue" "+")) -> ("something" "is" "young" "-"))
If something needs the cat and the cat is nice then it likes the lion.
((("something" "needs" "cat" "+") ("cat" "is" "nice" "+")) -> ("something" "likes" "lion" "+"))
The cat is not young.
True
1
proof
[(triple5 OR ((triple3) -> rule2))]
("cat" "is" "young" "-")
triple5
((triple3) -> (rule2 % int1))
The cat is not young.
("cat" "is" "young" "-")
int1
The cat is not nice.
False
1
inv-proof
[(triple4)]
("cat" "is" "nice" "-")
triple4
The lion likes the lion.
True
3
proof
[(((triple12 triple4) -> rule3))]
("lion" "likes" "lion" "+")
((triple12 triple4) -> (rule3 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1
The lion does not like the lion.
False
3
inv-proof
[(((triple12 triple4) -> rule3))]
("lion" "likes" "lion" "-")
((triple12 triple4) -> (rule3 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1
The cat does not like the lion.
Unknown
inv-rconc
[@1: The cat likes the lion.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cat" "likes" "lion" "-")
The tiger likes the lion.
Unknown
rconc
[@1: The tiger likes the lion.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("tiger" "likes" "lion" "+")
The tiger is not cold.
Unknown
inv-random
[@0: The tiger is cold.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "cold" "-")
The tiger is blue.
Unknown
random
[@0: The tiger is blue.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "blue" "+")
@0: The cat eats the tiger.[(triple1)] The cat is big.[(triple2)] The cat is blue.[(triple3)] The cat is nice.[(triple4)] The cat is not young.[(triple5 OR ((triple3) -> rule2))] The cat likes the tiger.[(triple6)] The cat needs the lion.[(triple7)] The lion eats the tiger.[(triple8)] The lion is not big.[(triple9)] The lion likes the cat.[(triple10)] The lion likes the tiger.[(triple11)] The lion needs the cat.[(triple12)] The lion needs the tiger.[(triple13)] The tiger does not need the cat.[(triple15)] The tiger is nice.[(triple14)] @1: The lion likes the lion.[(((triple12 triple4) -> rule3))]
The cat eats the tiger.
("cat" "eats" "tiger" "+")
triple1
The cat is big.
("cat" "is" "big" "+")
triple2
The cat is blue.
("cat" "is" "blue" "+")
triple3
The cat is nice.
("cat" "is" "nice" "+")
triple4
The cat is not young.
("cat" "is" "young" "-")
triple5
((triple3) -> (rule2 % int1))
The cat is not young.
("cat" "is" "young" "-")
int1
The cat likes the tiger.
("cat" "likes" "tiger" "+")
triple6
The cat needs the lion.
("cat" "needs" "lion" "+")
triple7
The lion eats the tiger.
("lion" "eats" "tiger" "+")
triple8
The lion is not big.
("lion" "is" "big" "-")
triple9
The lion likes the cat.
("lion" "likes" "cat" "+")
triple10
The lion likes the tiger.
("lion" "likes" "tiger" "+")
triple11
The lion needs the cat.
("lion" "needs" "cat" "+")
triple12
The lion needs the tiger.
("lion" "needs" "tiger" "+")
triple13
The tiger does not need the cat.
("tiger" "needs" "cat" "-")
triple15
The tiger is nice.
("tiger" "is" "nice" "+")
triple14
The lion likes the lion.
("lion" "likes" "lion" "+")
((triple12 triple4) -> (rule3 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1