The tiger is blue. The tiger is cold. The tiger is red. The tiger is rough. The tiger is round. If something is cold then it is round.
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger is red.
("tiger" "is" "red" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
The tiger is round.
("tiger" "is" "round" "+")
If something is cold then it is round.
((("something" "is" "cold" "+")) -> ("something" "is" "round" "+"))
The tiger is rough.
True
1
proof
[(triple4)]
("tiger" "is" "rough" "+")
triple4
The tiger is not round.
False
1
inv-proof
[(triple5 OR ((triple2) -> rule1))]
("tiger" "is" "round" "-")
triple5
((triple2) -> (rule1 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
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 blue.[(triple1)] The tiger is cold.[(triple2)] The tiger is red.[(triple3)] The tiger is rough.[(triple4)] The tiger is round.[(triple5 OR ((triple2) -> rule1))]
The tiger is blue.
("tiger" "is" "blue" "+")
triple1
The tiger is cold.
("tiger" "is" "cold" "+")
triple2
The tiger is red.
("tiger" "is" "red" "+")
triple3
The tiger is rough.
("tiger" "is" "rough" "+")
triple4
The tiger is round.
("tiger" "is" "round" "+")
triple5
((triple2) -> (rule1 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1