The tiger is cold. The tiger is green. The tiger is kind. The tiger is nice. The tiger is round. If someone is cold and kind then they are nice. Nice, cold people are round.
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger is green.
("tiger" "is" "green" "+")
The tiger is kind.
("tiger" "is" "kind" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
The tiger is round.
("tiger" "is" "round" "+")
If someone is cold and kind then they are nice.
((("someone" "is" "cold" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "nice" "+"))
Nice, cold people are round.
((("someone" "is" "nice" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "round" "+"))
The tiger is green.
True
1
proof
[(triple2)]
("tiger" "is" "green" "+")
triple2
The tiger is not cold.
False
1
inv-proof
[(triple1)]
("tiger" "is" "cold" "-")
triple1
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 needs the tiger.
Unknown
random
[@0: The tiger needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "tiger" "+")
@0: The tiger is cold.[(triple1)] The tiger is green.[(triple2)] The tiger is kind.[(triple3)] The tiger is nice.[(triple4 OR ((triple1 triple3) -> rule1))] The tiger is round.[(triple5 OR ((triple4 triple1) -> rule2) OR ((((triple1 triple3) -> rule1) triple1) -> rule2))]
The tiger is cold.
("tiger" "is" "cold" "+")
triple1
The tiger is green.
("tiger" "is" "green" "+")
triple2
The tiger is kind.
("tiger" "is" "kind" "+")
triple3
The tiger is nice.
("tiger" "is" "nice" "+")
triple4
((triple1 triple3) -> (rule1 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
The tiger is round.
("tiger" "is" "round" "+")
triple5
((triple4 triple1) -> (rule2 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
((((triple1 triple3) -> (rule1 % int2)) triple1) -> (rule2 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
int2