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