The cat needs the tiger. The rabbit is green. The tiger is big. The tiger is green. The tiger is nice. The tiger is red. The tiger is young. The tiger does not like the cat. The tiger likes the rabbit. The tiger needs the rabbit. The tiger sees the cat. The tiger sees the rabbit. If something likes the cat then the cat likes the tiger. If something is red then it does not see the tiger. If something needs the tiger then the tiger is red. If something needs the cat and it needs the tiger then the tiger likes the rabbit. If something sees the rabbit and it is not red then it is not nice. If the cat is not nice then the cat sees the tiger.
The cat needs the tiger.
("cat" "needs" "tiger" "+")
The rabbit is green.
("rabbit" "is" "green" "+")
The tiger is big.
("tiger" "is" "big" "+")
The tiger is green.
("tiger" "is" "green" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
The tiger is red.
("tiger" "is" "red" "+")
The tiger is young.
("tiger" "is" "young" "+")
The tiger does not like the cat.
("tiger" "likes" "cat" "-")
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
The tiger sees the cat.
("tiger" "sees" "cat" "+")
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
If something likes the cat then the cat likes the tiger.
((("something" "likes" "cat" "+")) -> ("cat" "likes" "tiger" "+"))
If something is red then it does not see the tiger.
((("something" "is" "red" "+")) -> ("something" "sees" "tiger" "-"))
If something needs the tiger then the tiger is red.
((("something" "needs" "tiger" "+")) -> ("tiger" "is" "red" "+"))
If something needs the cat and it needs the tiger then the tiger likes the rabbit.
((("something" "needs" "cat" "+") ("something" "needs" "tiger" "+")) -> ("tiger" "likes" "rabbit" "+"))
If something sees the rabbit and it is not red then it is not nice.
((("something" "sees" "rabbit" "+") ("something" "is" "red" "~")) -> ("something" "is" "nice" "-"))
If the cat is not nice then the cat sees the tiger.
((("cat" "is" "nice" "~")) -> ("cat" "sees" "tiger" "+"))
The tiger is nice.
True
1
proof
[(triple5)]
("tiger" "is" "nice" "+")
triple5
The cat does not need the tiger.
False
1
inv-proof
[(triple1)]
("cat" "needs" "tiger" "-")
triple1
The tiger does not see the tiger.
True
2
proof
[(((triple6) -> rule2) OR ((((triple1) -> rule3)) -> rule2))]
("tiger" "sees" "tiger" "-")
((triple6) -> (rule2 % int1))
The tiger does not see the tiger.
("tiger" "sees" "tiger" "-")
int1
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
The tiger does not see the tiger.
("tiger" "sees" "tiger" "-")
int1
The tiger is red.
("tiger" "is" "red" "+")
int2
The tiger sees the tiger.
False
2
inv-proof
[(((triple6) -> rule2) OR ((((triple1) -> rule3)) -> rule2))]
("tiger" "sees" "tiger" "+")
((triple6) -> (rule2 % int1))
The tiger does not see the tiger.
("tiger" "sees" "tiger" "-")
int1
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
The tiger does not see the tiger.
("tiger" "sees" "tiger" "-")
int1
The tiger is red.
("tiger" "is" "red" "+")
int2
The cat does not like the tiger.
Unknown
inv-rconc
[@1: The cat likes the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "likes" "tiger" "-")
The cat sees the tiger.
Unknown
rconc
[@1: The cat sees the tiger.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cat" "sees" "tiger" "+")
The tiger does not need the cat.
Unknown
inv-random
[@0: The tiger needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "cat" "-")
The rabbit sees the tiger.
Unknown
random
[@0: The rabbit sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "tiger" "+")
@0: The cat needs the tiger.[(triple1)] The rabbit is green.[(triple2)] The tiger does not like the cat.[(triple8)] The tiger is big.[(triple3)] The tiger is green.[(triple4)] The tiger is nice.[(triple5)] The tiger is red.[(triple6 OR ((triple1) -> rule3))] The tiger is young.[(triple7)] The tiger likes the rabbit.[(triple9)] The tiger needs the rabbit.[(triple10)] The tiger sees the cat.[(triple11)] The tiger sees the rabbit.[(triple12)] @1: The tiger does not see the tiger.[(((triple6) -> rule2) OR ((((triple1) -> rule3)) -> rule2))]
The cat needs the tiger.
("cat" "needs" "tiger" "+")
triple1
The rabbit is green.
("rabbit" "is" "green" "+")
triple2
The tiger does not like the cat.
("tiger" "likes" "cat" "-")
triple8
The tiger is big.
("tiger" "is" "big" "+")
triple3
The tiger is green.
("tiger" "is" "green" "+")
triple4
The tiger is nice.
("tiger" "is" "nice" "+")
triple5
The tiger is red.
("tiger" "is" "red" "+")
triple6
((triple1) -> (rule3 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
The tiger is young.
("tiger" "is" "young" "+")
triple7
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
triple9
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
triple10
The tiger sees the cat.
("tiger" "sees" "cat" "+")
triple11
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
triple12
The tiger does not see the tiger.
("tiger" "sees" "tiger" "-")
((triple6) -> (rule2 % int1))
The tiger does not see the tiger.
("tiger" "sees" "tiger" "-")
int1
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
The tiger does not see the tiger.
("tiger" "sees" "tiger" "-")
int1
The tiger is red.
("tiger" "is" "red" "+")
int2