The tiger is cold. The tiger is green. The tiger is not red. The tiger is rough. The tiger is young. Red, cold things are not young. If something is red and not rough then it is not green. If the tiger is green then the tiger is cold.
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger is green.
("tiger" "is" "green" "+")
The tiger is not red.
("tiger" "is" "red" "-")
The tiger is rough.
("tiger" "is" "rough" "+")
The tiger is young.
("tiger" "is" "young" "+")
Red, cold things are not young.
((("something" "is" "red" "+") ("something" "is" "cold" "+")) -> ("something" "is" "young" "-"))
If something is red and not rough then it is not green.
((("something" "is" "red" "+") ("something" "is" "rough" "~")) -> ("something" "is" "green" "-"))
If the tiger is green then the tiger is cold.
((("tiger" "is" "green" "+")) -> ("tiger" "is" "cold" "+"))
The tiger is cold.
True
1
proof
[(triple1 OR ((triple2) -> rule3))]
("tiger" "is" "cold" "+")
triple1
((triple2) -> (rule3 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger is red.
False
1
inv-proof
[(triple3)]
("tiger" "is" "red" "+")
triple3
The tiger does not see the tiger.
Unknown
inv-random
[@0: The tiger sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "tiger" "-")
The tiger likes the tiger.
Unknown
random
[@0: The tiger likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "tiger" "+")
@0: The tiger is cold.[(triple1 OR ((triple2) -> rule3))] The tiger is green.[(triple2)] The tiger is not red.[(triple3)] The tiger is rough.[(triple4)] The tiger is young.[(triple5)]
The tiger is cold.
("tiger" "is" "cold" "+")
triple1
((triple2) -> (rule3 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
triple2
The tiger is not red.
("tiger" "is" "red" "-")
triple3
The tiger is rough.
("tiger" "is" "rough" "+")
triple4
The tiger is young.
("tiger" "is" "young" "+")
triple5