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