The rabbit sees the tiger. The tiger is blue. The tiger is cold. If someone visits the rabbit then the rabbit is cold. If someone is cold then they visit the rabbit. If the rabbit sees the tiger then the tiger sees the rabbit.
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
If someone visits the rabbit then the rabbit is cold.
((("someone" "visits" "rabbit" "+")) -> ("rabbit" "is" "cold" "+"))
If someone is cold then they visit the rabbit.
((("someone" "is" "cold" "+")) -> ("someone" "visits" "rabbit" "+"))
If the rabbit sees the tiger then the tiger sees the rabbit.
((("rabbit" "sees" "tiger" "+")) -> ("tiger" "sees" "rabbit" "+"))
The tiger is cold.
True
1
proof
[(triple3)]
("tiger" "is" "cold" "+")
triple3
The tiger is not blue.
False
1
inv-proof
[(triple2)]
("tiger" "is" "blue" "-")
triple2
The tiger sees the rabbit.
True
2
proof
[(((triple1) -> rule3))]
("tiger" "sees" "rabbit" "+")
((triple1) -> (rule3 % int1))
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
int1
The tiger does not see the rabbit.
False
2
inv-proof
[(((triple1) -> rule3))]
("tiger" "sees" "rabbit" "-")
((triple1) -> (rule3 % int1))
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
int1
The rabbit is cold.
True
3
proof
[(((((triple3) -> rule2)) -> rule1))]
("rabbit" "is" "cold" "+")
((((triple3) -> (rule2 % int2))) -> (rule1 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
int2
The rabbit is not cold.
False
3
inv-proof
[(((((triple3) -> rule2)) -> rule1))]
("rabbit" "is" "cold" "-")
((((triple3) -> (rule2 % int2))) -> (rule1 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
int2
The rabbit visits the rabbit.
True
4
proof
[(((((((triple3) -> rule2)) -> rule1)) -> rule2))]
("rabbit" "visits" "rabbit" "+")
((((((triple3) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1
The rabbit is cold.
("rabbit" "is" "cold" "+")
int2
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
int3
The rabbit does not visit the rabbit.
False
4
inv-proof
[(((((((triple3) -> rule2)) -> rule1)) -> rule2))]
("rabbit" "visits" "rabbit" "-")
((((((triple3) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1
The rabbit is cold.
("rabbit" "is" "cold" "+")
int2
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
int3
The tiger does not like the rabbit.
Unknown
inv-random
[@0: The tiger likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "rabbit" "-")
The tiger is red.
Unknown
random
[@0: The tiger is red.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "red" "+")
The rabbit is not round.
Unknown
inv-random
[@0: The rabbit is round.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "round" "-")
The rabbit is red.
Unknown
random
[@0: The rabbit is red.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "red" "+")
The rabbit does not see the rabbit.
Unknown
inv-random
[@0: The rabbit sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "rabbit" "-")
The tiger visits the tiger.
Unknown
random
[@0: The tiger visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "tiger" "+")
The tiger does not like the tiger.
Unknown
inv-random
[@0: The tiger likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "tiger" "-")
The tiger is round.
Unknown
random
[@0: The tiger is round.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "round" "+")
@0: The rabbit sees the tiger.[(triple1)] The tiger is blue.[(triple2)] The tiger is cold.[(triple3)] @1: The tiger sees the rabbit.[(((triple1) -> rule3))] The tiger visits the rabbit.[(((triple3) -> rule2))] @2: The rabbit is cold.[(((((triple3) -> rule2)) -> rule1))] @3: The rabbit visits the rabbit.[(((((((triple3) -> rule2)) -> rule1)) -> rule2))]
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
triple1
The tiger is blue.
("tiger" "is" "blue" "+")
triple2
The tiger is cold.
("tiger" "is" "cold" "+")
triple3
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
((triple1) -> (rule3 % int1))
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
int1
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
((triple3) -> (rule2 % int1))
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
int1
The rabbit is cold.
("rabbit" "is" "cold" "+")
((((triple3) -> (rule2 % int2))) -> (rule1 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
int2
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
((((((triple3) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1
The rabbit is cold.
("rabbit" "is" "cold" "+")
int2
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
int3