The tiger is red. If the tiger is red and the tiger is green then the tiger is round. If something is red then it is rough.
The tiger is red.
("tiger" "is" "red" "+")
If the tiger is red and the tiger is green then the tiger is round.
((("tiger" "is" "red" "+") ("tiger" "is" "green" "+")) -> ("tiger" "is" "round" "+"))
If something is red then it is rough.
((("something" "is" "red" "+")) -> ("something" "is" "rough" "+"))
The tiger is red.
True
1
proof
[(triple1)]
("tiger" "is" "red" "+")
triple1
The tiger is not red.
False
1
inv-proof
[(triple1)]
("tiger" "is" "red" "-")
triple1
The tiger is rough.
True
2
proof
[(((triple1) -> rule2))]
("tiger" "is" "rough" "+")
((triple1) -> (rule2 % int1))
The tiger is rough.
("tiger" "is" "rough" "+")
int1
The tiger is not rough.
False
2
inv-proof
[(((triple1) -> rule2))]
("tiger" "is" "rough" "-")
((triple1) -> (rule2 % int1))
The tiger is rough.
("tiger" "is" "rough" "+")
int1
The tiger is not round.
Unknown
inv-rconc
[@1: The tiger is round.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "is" "round" "-")
The tiger needs the tiger.
Unknown
random
[@0: The tiger needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "tiger" "+")
The tiger is not green.
Unknown
inv-random
[@0: The tiger is green.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "green" "-")
The tiger visits the tiger.
Unknown
random
[@0: The tiger visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "tiger" "+")
@0: The tiger is red.[(triple1)] @1: The tiger is rough.[(((triple1) -> rule2))]
The tiger is red.
("tiger" "is" "red" "+")
triple1
The tiger is rough.
("tiger" "is" "rough" "+")
((triple1) -> (rule2 % int1))
The tiger is rough.
("tiger" "is" "rough" "+")
int1