The cat is not big. The tiger needs the cat. If something is nice and it chases the cat then it is not big. If something needs the cat then the cat needs the tiger. If the cat chases the tiger and the cat does not need the tiger then the tiger is young. If something needs the tiger then it likes the tiger. If something likes the cat then it likes the tiger. If something needs the cat and the cat does not need the tiger then it likes the tiger.
The cat is not big.
("cat" "is" "big" "-")
The tiger needs the cat.
("tiger" "needs" "cat" "+")
If something is nice and it chases the cat then it is not big.
((("something" "is" "nice" "+") ("something" "chases" "cat" "+")) -> ("something" "is" "big" "-"))
If something needs the cat then the cat needs the tiger.
((("something" "needs" "cat" "+")) -> ("cat" "needs" "tiger" "+"))
If the cat chases the tiger and the cat does not need the tiger then the tiger is young.
((("cat" "chases" "tiger" "+") ("cat" "needs" "tiger" "~")) -> ("tiger" "is" "young" "+"))
If something needs the tiger then it likes the tiger.
((("something" "needs" "tiger" "+")) -> ("something" "likes" "tiger" "+"))
If something likes the cat then it likes the tiger.
((("something" "likes" "cat" "+")) -> ("something" "likes" "tiger" "+"))
If something needs the cat and the cat does not need the tiger then it likes the tiger.
((("something" "needs" "cat" "+") ("cat" "needs" "tiger" "~")) -> ("something" "likes" "tiger" "+"))
The cat is not big.
True
1
proof
[(triple1)]
("cat" "is" "big" "-")
triple1
The cat is big.
False
1
inv-proof
[(triple1)]
("cat" "is" "big" "+")
triple1
The cat needs the tiger.
True
2
proof
[(((triple2) -> rule2))]
("cat" "needs" "tiger" "+")
((triple2) -> (rule2 % int1))
The cat needs the tiger.
("cat" "needs" "tiger" "+")
int1
The cat does not need the tiger.
False
2
inv-proof
[(((triple2) -> rule2))]
("cat" "needs" "tiger" "-")
((triple2) -> (rule2 % int1))
The cat needs the tiger.
("cat" "needs" "tiger" "+")
int1
The cat likes the tiger.
True
3
proof
[(((((triple2) -> rule2)) -> rule4))]
("cat" "likes" "tiger" "+")
((((triple2) -> (rule2 % int2))) -> (rule4 % int1))
The cat likes the tiger.
("cat" "likes" "tiger" "+")
int1
The cat needs the tiger.
("cat" "needs" "tiger" "+")
int2
The cat does not like the tiger.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule4))]
("cat" "likes" "tiger" "-")
((((triple2) -> (rule2 % int2))) -> (rule4 % int1))
The cat likes the tiger.
("cat" "likes" "tiger" "+")
int1
The cat needs the tiger.
("cat" "needs" "tiger" "+")
int2
The tiger does not like the tiger.
Unknown
inv-rconc
[@1: The tiger likes the tiger.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("tiger" "likes" "tiger" "-")
The tiger is young.
Unknown
rconc
[@1: The tiger is young.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("tiger" "is" "young" "+")
The tiger is not red.
Unknown
inv-random
[@0: The tiger is red.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "red" "-")
The cat needs the cat.
Unknown
random
[@0: The cat needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "cat" "+")
The tiger does not like the cat.
Unknown
inv-random
[@0: The tiger likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "cat" "-")
The tiger is round.
Unknown
random
[@0: The tiger is round.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "round" "+")
@0: The cat is not big.[(triple1)] The tiger needs the cat.[(triple2)] @1: The cat needs the tiger.[(((triple2) -> rule2))] @2: The cat likes the tiger.[(((((triple2) -> rule2)) -> rule4))]
The cat is not big.
("cat" "is" "big" "-")
triple1
The tiger needs the cat.
("tiger" "needs" "cat" "+")
triple2
The cat needs the tiger.
("cat" "needs" "tiger" "+")
((triple2) -> (rule2 % int1))
The cat needs the tiger.
("cat" "needs" "tiger" "+")
int1
The cat likes the tiger.
("cat" "likes" "tiger" "+")
((((triple2) -> (rule2 % int2))) -> (rule4 % int1))
The cat likes the tiger.
("cat" "likes" "tiger" "+")
int1
The cat needs the tiger.
("cat" "needs" "tiger" "+")
int2