The rabbit visits the tiger. The tiger is big. If the tiger is big then the tiger chases the rabbit. If someone chases the rabbit then the rabbit sees the tiger. If the tiger chases the rabbit and the rabbit sees the tiger then the tiger sees the rabbit.
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
The tiger is big.
("tiger" "is" "big" "+")
If the tiger is big then the tiger chases the rabbit.
((("tiger" "is" "big" "+")) -> ("tiger" "chases" "rabbit" "+"))
If someone chases the rabbit then the rabbit sees the tiger.
((("someone" "chases" "rabbit" "+")) -> ("rabbit" "sees" "tiger" "+"))
If the tiger chases the rabbit and the rabbit sees the tiger then the tiger sees the rabbit.
((("tiger" "chases" "rabbit" "+") ("rabbit" "sees" "tiger" "+")) -> ("tiger" "sees" "rabbit" "+"))
The rabbit visits the tiger.
True
1
proof
[(triple1)]
("rabbit" "visits" "tiger" "+")
triple1
The tiger is not big.
False
1
inv-proof
[(triple2)]
("tiger" "is" "big" "-")
triple2
The tiger chases the rabbit.
True
2
proof
[(((triple2) -> rule1))]
("tiger" "chases" "rabbit" "+")
((triple2) -> (rule1 % int1))
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
int1
The tiger does not chase the rabbit.
False
2
inv-proof
[(((triple2) -> rule1))]
("tiger" "chases" "rabbit" "-")
((triple2) -> (rule1 % int1))
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
int1
The rabbit sees the tiger.
True
3
proof
[(((((triple2) -> rule1)) -> rule2))]
("rabbit" "sees" "tiger" "+")
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
int1
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
int2
The rabbit does not see the tiger.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule2))]
("rabbit" "sees" "tiger" "-")
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
int1
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
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 rabbit is rough.
Unknown
random
[@0: The rabbit is rough.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "rough" "+")
The tiger does not visit the rabbit.
Unknown
inv-random
[@0: The tiger visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "rabbit" "-")
The tiger sees the tiger.
Unknown
random
[@0: The tiger sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "tiger" "+")
The rabbit is not blue.
Unknown
inv-random
[@0: The rabbit is blue.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "blue" "-")
The tiger is kind.
Unknown
random
[@0: The tiger is kind.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "kind" "+")
@0: The rabbit visits the tiger.[(triple1)] The tiger is big.[(triple2)] @1: The tiger chases the rabbit.[(((triple2) -> rule1))] @2: The rabbit sees the tiger.[(((((triple2) -> rule1)) -> rule2))] @3: The tiger sees the rabbit.[(((((triple2) -> rule1) ((((triple2) -> rule1)) -> rule2)) -> rule3))]
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
triple1
The tiger is big.
("tiger" "is" "big" "+")
triple2
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
((triple2) -> (rule1 % int1))
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
int1
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
int1
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
int2
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
((((triple2) -> (rule1 % int3)) ((((triple2) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
int1
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
int2
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
int3