The cat chases the tiger. The cat is big. The cat is cold. The cat is green. The cat is kind. The cat likes the tiger. The cat needs the tiger. The tiger chases the cat. The tiger is big. The tiger is cold. The tiger is green. The tiger is kind. The tiger is young. The tiger likes the cat. The tiger needs the cat. If someone chases the cat and the cat likes the tiger then they are young. If someone is kind then they chase the cat. If someone chases the cat and they need the cat then they like the cat.
The cat chases the tiger.
("cat" "chases" "tiger" "+")
The cat is big.
("cat" "is" "big" "+")
The cat is cold.
("cat" "is" "cold" "+")
The cat is green.
("cat" "is" "green" "+")
The cat is kind.
("cat" "is" "kind" "+")
The cat likes the tiger.
("cat" "likes" "tiger" "+")
The cat needs the tiger.
("cat" "needs" "tiger" "+")
The tiger chases the cat.
("tiger" "chases" "cat" "+")
The tiger is big.
("tiger" "is" "big" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger is green.
("tiger" "is" "green" "+")
The tiger is kind.
("tiger" "is" "kind" "+")
The tiger is young.
("tiger" "is" "young" "+")
The tiger likes the cat.
("tiger" "likes" "cat" "+")
The tiger needs the cat.
("tiger" "needs" "cat" "+")
If someone chases the cat and the cat likes the tiger then they are young.
((("someone" "chases" "cat" "+") ("cat" "likes" "tiger" "+")) -> ("someone" "is" "young" "+"))
If someone is kind then they chase the cat.
((("someone" "is" "kind" "+")) -> ("someone" "chases" "cat" "+"))
If someone chases the cat and they need the cat then they like the cat.
((("someone" "chases" "cat" "+") ("someone" "needs" "cat" "+")) -> ("someone" "likes" "cat" "+"))
The tiger needs the cat.
True
1
proof
[(triple15)]
("tiger" "needs" "cat" "+")
triple15
The tiger is not green.
False
1
inv-proof
[(triple11)]
("tiger" "is" "green" "-")
triple11
The cat chases the cat.
True
2
proof
[(((triple5) -> rule2))]
("cat" "chases" "cat" "+")
((triple5) -> (rule2 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1
The cat does not chase the cat.
False
2
inv-proof
[(((triple5) -> rule2))]
("cat" "chases" "cat" "-")
((triple5) -> (rule2 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1
The cat does not like the cat.
Unknown
inv-rconc
[@1: The cat likes the cat.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cat" "likes" "cat" "-")
The tiger chases the tiger.
Unknown
random
[@0: The tiger chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "tiger" "+")
The cat does not need the cat.
Unknown
inv-random
[@0: The cat needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "cat" "-")
The tiger needs the tiger.
Unknown
random
[@0: The tiger needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "tiger" "+")
@0: The cat chases the tiger.[(triple1)] The cat is big.[(triple2)] The cat is cold.[(triple3)] The cat is green.[(triple4)] The cat is kind.[(triple5)] The cat likes the tiger.[(triple6)] The cat needs the tiger.[(triple7)] The tiger chases the cat.[(triple8 OR ((triple12) -> rule2))] The tiger is big.[(triple9)] The tiger is cold.[(triple10)] The tiger is green.[(triple11)] The tiger is kind.[(triple12)] The tiger is young.[(triple13 OR ((triple8 triple6) -> rule1) OR ((((triple12) -> rule2) triple6) -> rule1))] The tiger likes the cat.[(triple14 OR ((triple8 triple15) -> rule3) OR ((((triple12) -> rule2) triple15) -> rule3))] The tiger needs the cat.[(triple15)] @1: The cat chases the cat.[(((triple5) -> rule2))] @2: The cat is young.[(((((triple5) -> rule2) triple6) -> rule1))]
The cat chases the tiger.
("cat" "chases" "tiger" "+")
triple1
The cat is big.
("cat" "is" "big" "+")
triple2
The cat is cold.
("cat" "is" "cold" "+")
triple3
The cat is green.
("cat" "is" "green" "+")
triple4
The cat is kind.
("cat" "is" "kind" "+")
triple5
The cat likes the tiger.
("cat" "likes" "tiger" "+")
triple6
The cat needs the tiger.
("cat" "needs" "tiger" "+")
triple7
The tiger chases the cat.
("tiger" "chases" "cat" "+")
triple8
((triple12) -> (rule2 % int1))
The tiger chases the cat.
("tiger" "chases" "cat" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
triple9
The tiger is cold.
("tiger" "is" "cold" "+")
triple10
The tiger is green.
("tiger" "is" "green" "+")
triple11
The tiger is kind.
("tiger" "is" "kind" "+")
triple12
The tiger is young.
("tiger" "is" "young" "+")
triple13
((triple8 triple6) -> (rule1 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
((((triple12) -> (rule2 % int2)) triple6) -> (rule1 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The tiger chases the cat.
("tiger" "chases" "cat" "+")
int2
The tiger likes the cat.
("tiger" "likes" "cat" "+")
triple14
((triple8 triple15) -> (rule3 % int1))
The tiger likes the cat.
("tiger" "likes" "cat" "+")
int1
((((triple12) -> (rule2 % int2)) triple15) -> (rule3 % int1))
The tiger likes the cat.
("tiger" "likes" "cat" "+")
int1
The tiger chases the cat.
("tiger" "chases" "cat" "+")
int2
The tiger needs the cat.
("tiger" "needs" "cat" "+")
triple15
The cat chases the cat.
("cat" "chases" "cat" "+")
((triple5) -> (rule2 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1
The cat is young.
("cat" "is" "young" "+")
((((triple5) -> (rule2 % int2)) triple6) -> (rule1 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
The cat chases the cat.
("cat" "chases" "cat" "+")
int2