The tiger is cold. The tiger is nice. The tiger is not rough. Nice people are red. All rough people are kind.
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
The tiger is not rough.
("tiger" "is" "rough" "-")
Nice people are red.
((("someone" "is" "nice" "+")) -> ("someone" "is" "red" "+"))
All rough people are kind.
((("someone" "is" "rough" "+")) -> ("someone" "is" "kind" "+"))
The tiger is cold.
True
1
proof
[(triple1)]
("tiger" "is" "cold" "+")
triple1
The tiger is not nice.
False
1
inv-proof
[(triple2)]
("tiger" "is" "nice" "-")
triple2
The tiger is red.
True
2
proof
[(((triple2) -> rule1))]
("tiger" "is" "red" "+")
((triple2) -> (rule1 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
The tiger is not red.
False
2
inv-proof
[(((triple2) -> rule1))]
("tiger" "is" "red" "-")
((triple2) -> (rule1 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
The tiger is not kind.
Unknown
inv-rconc
[@1: The tiger is kind.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "is" "kind" "-")
The tiger chases the tiger.
Unknown
random
[@0: The tiger chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "tiger" "+")
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 visits the tiger.
Unknown
random
[@0: The tiger visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "tiger" "+")
@0: The tiger is cold.[(triple1)] The tiger is nice.[(triple2)] The tiger is not rough.[(triple3)] @1: The tiger is red.[(((triple2) -> rule1))]
The tiger is cold.
("tiger" "is" "cold" "+")
triple1
The tiger is nice.
("tiger" "is" "nice" "+")
triple2
The tiger is not rough.
("tiger" "is" "rough" "-")
triple3
The tiger is red.
("tiger" "is" "red" "+")
((triple2) -> (rule1 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1