The tiger is kind. Rough, nice things are kind. If the tiger is kind then the tiger is big. If something is blue and kind then it is nice. If the tiger is nice and the tiger is kind then the tiger is blue. If something is nice and blue then it is rough. All blue things are nice.
The tiger is kind.
("tiger" "is" "kind" "+")
Rough, nice things are kind.
((("something" "is" "rough" "+") ("something" "is" "nice" "+")) -> ("something" "is" "kind" "+"))
If the tiger is kind then the tiger is big.
((("tiger" "is" "kind" "+")) -> ("tiger" "is" "big" "+"))
If something is blue and kind then it is nice.
((("something" "is" "blue" "+") ("something" "is" "kind" "+")) -> ("something" "is" "nice" "+"))
If the tiger is nice and the tiger is kind then the tiger is blue.
((("tiger" "is" "nice" "+") ("tiger" "is" "kind" "+")) -> ("tiger" "is" "blue" "+"))
If something is nice and blue then it is rough.
((("something" "is" "nice" "+") ("something" "is" "blue" "+")) -> ("something" "is" "rough" "+"))
All blue things are nice.
((("something" "is" "blue" "+")) -> ("something" "is" "nice" "+"))
The tiger is kind.
True
1
proof
[(triple1)]
("tiger" "is" "kind" "+")
triple1
The tiger is not kind.
False
1
inv-proof
[(triple1)]
("tiger" "is" "kind" "-")
triple1
The tiger is big.
True
2
proof
[(((triple1) -> rule2))]
("tiger" "is" "big" "+")
((triple1) -> (rule2 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger is not big.
False
2
inv-proof
[(((triple1) -> rule2))]
("tiger" "is" "big" "-")
((triple1) -> (rule2 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger is not blue.
Unknown
inv-rconc
[@2: The tiger is blue.[CWA. Example of deepest failure = (rule4 <- rule3 <- FAIL)]]
("tiger" "is" "blue" "-")
The tiger is nice.
Unknown
rconc
[@3: The tiger is nice.[CWA. Example of deepest failure = (rule3 <- rule4 <- rule6 <- FAIL)]]
("tiger" "is" "nice" "+")
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 tiger needs the tiger.
Unknown
random
[@0: The tiger needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "tiger" "+")
@0: The tiger is kind.[(triple1)] @1: The tiger is big.[(((triple1) -> rule2))]
The tiger is kind.
("tiger" "is" "kind" "+")
triple1
The tiger is big.
("tiger" "is" "big" "+")
((triple1) -> (rule2 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1