The tiger is not big. The tiger is blue. The tiger is cold. The tiger is kind. The tiger is red. If something is cold then it is not big. If something is blue and red then it is kind.
The tiger is not big.
("tiger" "is" "big" "-")
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger is kind.
("tiger" "is" "kind" "+")
The tiger is red.
("tiger" "is" "red" "+")
If something is cold then it is not big.
((("something" "is" "cold" "+")) -> ("something" "is" "big" "-"))
If something is blue and red then it is kind.
((("something" "is" "blue" "+") ("something" "is" "red" "+")) -> ("something" "is" "kind" "+"))
The tiger is blue.
True
1
proof
[(triple2)]
("tiger" "is" "blue" "+")
triple2
The tiger is not cold.
False
1
inv-proof
[(triple3)]
("tiger" "is" "cold" "-")
triple3
The tiger does not chase the tiger.
Unknown
inv-random
[@0: The tiger chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "tiger" "-")
The tiger eats the tiger.
Unknown
random
[@0: The tiger eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "tiger" "+")
@0: The tiger is blue.[(triple2)] The tiger is cold.[(triple3)] The tiger is kind.[(triple4 OR ((triple2 triple5) -> rule2))] The tiger is not big.[(triple1 OR ((triple3) -> rule1))] The tiger is red.[(triple5)]
The tiger is blue.
("tiger" "is" "blue" "+")
triple2
The tiger is cold.
("tiger" "is" "cold" "+")
triple3
The tiger is kind.
("tiger" "is" "kind" "+")
triple4
((triple2 triple5) -> (rule2 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The tiger is not big.
("tiger" "is" "big" "-")
triple1
((triple3) -> (rule1 % int1))
The tiger is not big.
("tiger" "is" "big" "-")
int1
The tiger is red.
("tiger" "is" "red" "+")
triple5