The rabbit sees the tiger. The tiger is round. If someone sees the rabbit then they see the tiger. If someone sees the tiger and they see the rabbit then the rabbit is big. If someone is round then they see the rabbit.
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
The tiger is round.
("tiger" "is" "round" "+")
If someone sees the rabbit then they see the tiger.
((("someone" "sees" "rabbit" "+")) -> ("someone" "sees" "tiger" "+"))
If someone sees the tiger and they see the rabbit then the rabbit is big.
((("someone" "sees" "tiger" "+") ("someone" "sees" "rabbit" "+")) -> ("rabbit" "is" "big" "+"))
If someone is round then they see the rabbit.
((("someone" "is" "round" "+")) -> ("someone" "sees" "rabbit" "+"))
The tiger is round.
True
1
proof
[(triple2)]
("tiger" "is" "round" "+")
triple2
The tiger is not round.
False
1
inv-proof
[(triple2)]
("tiger" "is" "round" "-")
triple2
The tiger sees the rabbit.
True
2
proof
[(((triple2) -> rule3))]
("tiger" "sees" "rabbit" "+")
((triple2) -> (rule3 % int1))
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
int1
The tiger does not see the rabbit.
False
2
inv-proof
[(((triple2) -> rule3))]
("tiger" "sees" "rabbit" "-")
((triple2) -> (rule3 % int1))
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
int1
The tiger sees the tiger.
True
3
proof
[(((((triple2) -> rule3)) -> rule1))]
("tiger" "sees" "tiger" "+")
((((triple2) -> (rule3 % int2))) -> (rule1 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
int2
The tiger does not see the tiger.
False
3
inv-proof
[(((((triple2) -> rule3)) -> rule1))]
("tiger" "sees" "tiger" "-")
((((triple2) -> (rule3 % int2))) -> (rule1 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
int2
The rabbit does not see the rabbit.
Unknown
inv-rconc
[@1: The rabbit sees the rabbit.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("rabbit" "sees" "rabbit" "-")
The rabbit is red.
Unknown
random
[@0: The rabbit is red.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "red" "+")
The tiger is not rough.
Unknown
inv-random
[@0: The tiger is rough.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "rough" "-")
The tiger is red.
Unknown
random
[@0: The tiger is red.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "red" "+")
The tiger does not eat the tiger.
Unknown
inv-random
[@0: The tiger eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "tiger" "-")
The rabbit is round.
Unknown
random
[@0: The rabbit is round.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "round" "+")
@0: The rabbit sees the tiger.[(triple1)] The tiger is round.[(triple2)] @1: The tiger sees the rabbit.[(((triple2) -> rule3))] @2: The tiger sees the tiger.[(((((triple2) -> rule3)) -> rule1))] @3: The rabbit is big.[(((((((triple2) -> rule3)) -> rule1) ((triple2) -> rule3)) -> rule2))]
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
triple1
The tiger is round.
("tiger" "is" "round" "+")
triple2
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
((triple2) -> (rule3 % int1))
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
int1
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
((((triple2) -> (rule3 % int2))) -> (rule1 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
int2
The rabbit is big.
("rabbit" "is" "big" "+")
((((((triple2) -> (rule3 % int3))) -> (rule1 % int2)) ((triple2) -> (rule3 % int3))) -> (rule2 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int2
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
int3