The tiger is big. The tiger is blue. The tiger is not nice. The tiger is not red. The tiger is young. If the tiger is blue and the tiger is not nice then the tiger is not red. If something is young then it is blue. If something is red and nice then it is big.
The tiger is big.
("tiger" "is" "big" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger is not nice.
("tiger" "is" "nice" "-")
The tiger is not red.
("tiger" "is" "red" "-")
The tiger is young.
("tiger" "is" "young" "+")
If the tiger is blue and the tiger is not nice then the tiger is not red.
((("tiger" "is" "blue" "+") ("tiger" "is" "nice" "~")) -> ("tiger" "is" "red" "-"))
If something is young then it is blue.
((("something" "is" "young" "+")) -> ("something" "is" "blue" "+"))
If something is red and nice then it is big.
((("something" "is" "red" "+") ("something" "is" "nice" "+")) -> ("something" "is" "big" "+"))
The tiger is not nice.
True
1
proof
[(triple3)]
("tiger" "is" "nice" "-")
triple3
The tiger is not big.
False
1
inv-proof
[(triple1)]
("tiger" "is" "big" "-")
triple1
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 OR ((triple5) -> rule2))] The tiger is not nice.[(triple3)] The tiger is not red.[(triple4 OR ((triple2 triple3) -> rule1) OR ((((triple5) -> rule2) triple3) -> rule1))] The tiger is young.[(triple5)]
The tiger is big.
("tiger" "is" "big" "+")
triple1
The tiger is blue.
("tiger" "is" "blue" "+")
triple2
((triple5) -> (rule2 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The tiger is not nice.
("tiger" "is" "nice" "-")
triple3
The tiger is not red.
("tiger" "is" "red" "-")
triple4
((triple2 triple3) -> (rule1 % int1))
The tiger is not red.
("tiger" "is" "red" "-")
int1
((((triple5) -> (rule2 % int2)) triple3) -> (rule1 % int1))
The tiger is not red.
("tiger" "is" "red" "-")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
int2
The tiger is young.
("tiger" "is" "young" "+")
triple5