The cat chases the tiger. The cat is big. The cat is blue. The cat is cold. The cat is red. The cat is rough. The cat likes the tiger. The cat visits the tiger. The tiger chases the cat. The tiger is big. The tiger is blue. The tiger is cold. The tiger is red. The tiger is rough. The tiger likes the cat. The tiger visits the cat. If something chases the cat then it likes the cat. If something visits the cat then the cat chases the tiger. If something is cold then it chases the cat.
The cat chases the tiger.
("cat" "chases" "tiger" "+")
The cat is big.
("cat" "is" "big" "+")
The cat is blue.
("cat" "is" "blue" "+")
The cat is cold.
("cat" "is" "cold" "+")
The cat is red.
("cat" "is" "red" "+")
The cat is rough.
("cat" "is" "rough" "+")
The cat likes the tiger.
("cat" "likes" "tiger" "+")
The cat visits the tiger.
("cat" "visits" "tiger" "+")
The tiger chases the cat.
("tiger" "chases" "cat" "+")
The tiger is big.
("tiger" "is" "big" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger is red.
("tiger" "is" "red" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
The tiger likes the cat.
("tiger" "likes" "cat" "+")
The tiger visits the cat.
("tiger" "visits" "cat" "+")
If something chases the cat then it likes the cat.
((("something" "chases" "cat" "+")) -> ("something" "likes" "cat" "+"))
If something visits the cat then the cat chases the tiger.
((("something" "visits" "cat" "+")) -> ("cat" "chases" "tiger" "+"))
If something is cold then it chases the cat.
((("something" "is" "cold" "+")) -> ("something" "chases" "cat" "+"))
The cat is cold.
True
1
proof
[(triple4)]
("cat" "is" "cold" "+")
triple4
The tiger is not red.
False
1
inv-proof
[(triple13)]
("tiger" "is" "red" "-")
triple13
The cat chases the cat.
True
2
proof
[(((triple4) -> rule3))]
("cat" "chases" "cat" "+")
((triple4) -> (rule3 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1
The cat does not chase the cat.
False
2
inv-proof
[(((triple4) -> rule3))]
("cat" "chases" "cat" "-")
((triple4) -> (rule3 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1
The cat likes the cat.
True
3
proof
[(((((triple4) -> rule3)) -> rule1))]
("cat" "likes" "cat" "+")
((((triple4) -> (rule3 % int2))) -> (rule1 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The cat chases the cat.
("cat" "chases" "cat" "+")
int2
The cat does not like the cat.
False
3
inv-proof
[(((((triple4) -> rule3)) -> rule1))]
("cat" "likes" "cat" "-")
((((triple4) -> (rule3 % int2))) -> (rule1 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The cat chases the cat.
("cat" "chases" "cat" "+")
int2
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 tiger likes the tiger.
Unknown
random
[@0: The tiger likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "tiger" "+")
The tiger does not visit the tiger.
Unknown
inv-random
[@0: The tiger visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "tiger" "-")
The cat visits the cat.
Unknown
random
[@0: The cat visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "cat" "+")
@0: The cat chases the tiger.[(triple1 OR ((triple16) -> rule2))] The cat is big.[(triple2)] The cat is blue.[(triple3)] The cat is cold.[(triple4)] The cat is red.[(triple5)] The cat is rough.[(triple6)] The cat likes the tiger.[(triple7)] The cat visits the tiger.[(triple8)] The tiger chases the cat.[(triple9 OR ((triple12) -> rule3))] The tiger is big.[(triple10)] The tiger is blue.[(triple11)] The tiger is cold.[(triple12)] The tiger is red.[(triple13)] The tiger is rough.[(triple14)] The tiger likes the cat.[(triple15 OR ((triple9) -> rule1) OR ((((triple12) -> rule3)) -> rule1))] The tiger visits the cat.[(triple16)] @1: The cat chases the cat.[(((triple4) -> rule3))] @2: The cat likes the cat.[(((((triple4) -> rule3)) -> rule1))]
The cat chases the tiger.
("cat" "chases" "tiger" "+")
triple1
((triple16) -> (rule2 % int1))
The cat chases the tiger.
("cat" "chases" "tiger" "+")
int1
The cat is big.
("cat" "is" "big" "+")
triple2
The cat is blue.
("cat" "is" "blue" "+")
triple3
The cat is cold.
("cat" "is" "cold" "+")
triple4
The cat is red.
("cat" "is" "red" "+")
triple5
The cat is rough.
("cat" "is" "rough" "+")
triple6
The cat likes the tiger.
("cat" "likes" "tiger" "+")
triple7
The cat visits the tiger.
("cat" "visits" "tiger" "+")
triple8
The tiger chases the cat.
("tiger" "chases" "cat" "+")
triple9
((triple12) -> (rule3 % int1))
The tiger chases the cat.
("tiger" "chases" "cat" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
triple10
The tiger is blue.
("tiger" "is" "blue" "+")
triple11
The tiger is cold.
("tiger" "is" "cold" "+")
triple12
The tiger is red.
("tiger" "is" "red" "+")
triple13
The tiger is rough.
("tiger" "is" "rough" "+")
triple14
The tiger likes the cat.
("tiger" "likes" "cat" "+")
triple15
((triple9) -> (rule1 % int1))
The tiger likes the cat.
("tiger" "likes" "cat" "+")
int1
((((triple12) -> (rule3 % int2))) -> (rule1 % int1))
The tiger likes the cat.
("tiger" "likes" "cat" "+")
int1
The tiger chases the cat.
("tiger" "chases" "cat" "+")
int2
The tiger visits the cat.
("tiger" "visits" "cat" "+")
triple16
The cat chases the cat.
("cat" "chases" "cat" "+")
((triple4) -> (rule3 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1
The cat likes the cat.
("cat" "likes" "cat" "+")
((((triple4) -> (rule3 % int2))) -> (rule1 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The cat chases the cat.
("cat" "chases" "cat" "+")
int2