The cat likes the tiger. The cat sees the tiger. The tiger chases the cat. The tiger is kind. The tiger is red. The tiger is rough. The tiger sees the cat. If something is rough and it likes the tiger then it sees the cat. If something sees the tiger then the tiger likes the cat. If something likes the cat and it chases the cat then the cat chases the tiger. If the tiger is young then the tiger sees the cat. If something chases the tiger and the tiger sees the cat then the cat is rough. If something likes the tiger and the tiger is young then the tiger sees the cat.
The cat likes the tiger.
("cat" "likes" "tiger" "+")
The cat sees the tiger.
("cat" "sees" "tiger" "+")
The tiger chases the cat.
("tiger" "chases" "cat" "+")
The tiger is kind.
("tiger" "is" "kind" "+")
The tiger is red.
("tiger" "is" "red" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
The tiger sees the cat.
("tiger" "sees" "cat" "+")
If something is rough and it likes the tiger then it sees the cat.
((("something" "is" "rough" "+") ("something" "likes" "tiger" "+")) -> ("something" "sees" "cat" "+"))
If something sees the tiger then the tiger likes the cat.
((("something" "sees" "tiger" "+")) -> ("tiger" "likes" "cat" "+"))
If something likes the cat and it chases the cat then the cat chases the tiger.
((("something" "likes" "cat" "+") ("something" "chases" "cat" "+")) -> ("cat" "chases" "tiger" "+"))
If the tiger is young then the tiger sees the cat.
((("tiger" "is" "young" "+")) -> ("tiger" "sees" "cat" "+"))
If something chases the tiger and the tiger sees the cat then the cat is rough.
((("something" "chases" "tiger" "+") ("tiger" "sees" "cat" "+")) -> ("cat" "is" "rough" "+"))
If something likes the tiger and the tiger is young then the tiger sees the cat.
((("something" "likes" "tiger" "+") ("tiger" "is" "young" "+")) -> ("tiger" "sees" "cat" "+"))
The tiger chases the cat.
True
1
proof
[(triple3)]
("tiger" "chases" "cat" "+")
triple3
The tiger is not red.
False
1
inv-proof
[(triple5)]
("tiger" "is" "red" "-")
triple5
The tiger likes the cat.
True
2
proof
[(((triple2) -> rule2))]
("tiger" "likes" "cat" "+")
((triple2) -> (rule2 % int1))
The tiger likes the cat.
("tiger" "likes" "cat" "+")
int1
The tiger does not like the cat.
False
2
inv-proof
[(((triple2) -> rule2))]
("tiger" "likes" "cat" "-")
((triple2) -> (rule2 % int1))
The tiger likes the cat.
("tiger" "likes" "cat" "+")
int1
The cat chases the tiger.
True
4
proof
[(((((triple2) -> rule2) triple3) -> rule3))]
("cat" "chases" "tiger" "+")
((((triple2) -> (rule2 % int2)) triple3) -> (rule3 % int1))
The cat chases the tiger.
("cat" "chases" "tiger" "+")
int1
The tiger likes the cat.
("tiger" "likes" "cat" "+")
int2
The cat does not chase the tiger.
False
4
inv-proof
[(((((triple2) -> rule2) triple3) -> rule3))]
("cat" "chases" "tiger" "-")
((((triple2) -> (rule2 % int2)) triple3) -> (rule3 % int1))
The cat chases the tiger.
("cat" "chases" "tiger" "+")
int1
The tiger likes the cat.
("tiger" "likes" "cat" "+")
int2
The cat is rough.
True
6
proof
[(((((((triple2) -> rule2) triple3) -> rule3) triple7) -> rule5))]
("cat" "is" "rough" "+")
((((((triple2) -> (rule2 % int3)) triple3) -> (rule3 % int2)) triple7) -> (rule5 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The cat chases the tiger.
("cat" "chases" "tiger" "+")
int2
The tiger likes the cat.
("tiger" "likes" "cat" "+")
int3
The cat is not rough.
False
6
inv-proof
[(((((((triple2) -> rule2) triple3) -> rule3) triple7) -> rule5))]
("cat" "is" "rough" "-")
((((((triple2) -> (rule2 % int3)) triple3) -> (rule3 % int2)) triple7) -> (rule5 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The cat chases the tiger.
("cat" "chases" "tiger" "+")
int2
The tiger likes the cat.
("tiger" "likes" "cat" "+")
int3
The cat does not like the cat.
Unknown
inv-random
[@0: The cat likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "cat" "-")
The tiger likes the tiger.
Unknown
random
[@0: The tiger likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "tiger" "+")
The cat is not kind.
Unknown
inv-random
[@0: The cat is kind.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "kind" "-")
The cat is young.
Unknown
random
[@0: The cat is young.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "young" "+")
The tiger does not chase the tiger.
Unknown
inv-random
[@0: The tiger chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "tiger" "-")
The cat is big.
Unknown
random
[@0: The cat is big.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "big" "+")
The tiger is not big.
Unknown
inv-random
[@0: The tiger is big.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "big" "-")
The cat is red.
Unknown
random
[@0: The cat is red.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "red" "+")
@0: The cat likes the tiger.[(triple1)] The cat sees the tiger.[(triple2)] The tiger chases the cat.[(triple3)] The tiger is kind.[(triple4)] The tiger is red.[(triple5)] The tiger is rough.[(triple6)] The tiger sees the cat.[(triple7)] @1: The tiger likes the cat.[(((triple2) -> rule2))] @2: The cat chases the tiger.[(((((triple2) -> rule2) triple3) -> rule3))] @3: The cat is rough.[(((((((triple2) -> rule2) triple3) -> rule3) triple7) -> rule5))] @4: The cat sees the cat.[(((((((((triple2) -> rule2) triple3) -> rule3) triple7) -> rule5) triple1) -> rule1))]
The cat likes the tiger.
("cat" "likes" "tiger" "+")
triple1
The cat sees the tiger.
("cat" "sees" "tiger" "+")
triple2
The tiger chases the cat.
("tiger" "chases" "cat" "+")
triple3
The tiger is kind.
("tiger" "is" "kind" "+")
triple4
The tiger is red.
("tiger" "is" "red" "+")
triple5
The tiger is rough.
("tiger" "is" "rough" "+")
triple6
The tiger sees the cat.
("tiger" "sees" "cat" "+")
triple7
The tiger likes the cat.
("tiger" "likes" "cat" "+")
((triple2) -> (rule2 % int1))
The tiger likes the cat.
("tiger" "likes" "cat" "+")
int1
The cat chases the tiger.
("cat" "chases" "tiger" "+")
((((triple2) -> (rule2 % int2)) triple3) -> (rule3 % int1))
The cat chases the tiger.
("cat" "chases" "tiger" "+")
int1
The tiger likes the cat.
("tiger" "likes" "cat" "+")
int2
The cat is rough.
("cat" "is" "rough" "+")
((((((triple2) -> (rule2 % int3)) triple3) -> (rule3 % int2)) triple7) -> (rule5 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The cat chases the tiger.
("cat" "chases" "tiger" "+")
int2
The tiger likes the cat.
("tiger" "likes" "cat" "+")
int3
The cat sees the cat.
("cat" "sees" "cat" "+")
((((((((triple2) -> (rule2 % int4)) triple3) -> (rule3 % int3)) triple7) -> (rule5 % int2)) triple1) -> (rule1 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
The cat is rough.
("cat" "is" "rough" "+")
int2
The cat chases the tiger.
("cat" "chases" "tiger" "+")
int3
The tiger likes the cat.
("tiger" "likes" "cat" "+")
int4