The tiger is blue. The tiger is kind. The tiger is nice. The tiger is rough. The tiger is not round. If the tiger is round and the tiger is nice then the tiger is rough. If the tiger is blue then the tiger is rough. If something is rough and not blue then it is nice. If something is nice and rough then it is kind. Nice, round things are kind. If something is kind and not blue then it is rough.
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger is kind.
("tiger" "is" "kind" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
The tiger is not round.
("tiger" "is" "round" "-")
If the tiger is round and the tiger is nice then the tiger is rough.
((("tiger" "is" "round" "+") ("tiger" "is" "nice" "+")) -> ("tiger" "is" "rough" "+"))
If the tiger is blue then the tiger is rough.
((("tiger" "is" "blue" "+")) -> ("tiger" "is" "rough" "+"))
If something is rough and not blue then it is nice.
((("something" "is" "rough" "+") ("something" "is" "blue" "~")) -> ("something" "is" "nice" "+"))
If something is nice and rough then it is kind.
((("something" "is" "nice" "+") ("something" "is" "rough" "+")) -> ("something" "is" "kind" "+"))
Nice, round things are kind.
((("something" "is" "nice" "+") ("something" "is" "round" "+")) -> ("something" "is" "kind" "+"))
If something is kind and not blue then it is rough.
((("something" "is" "kind" "+") ("something" "is" "blue" "~")) -> ("something" "is" "rough" "+"))
The tiger is rough.
True
1
proof
[(triple4 OR ((triple1) -> rule2))]
("tiger" "is" "rough" "+")
triple4
((triple1) -> (rule2 % int1))
The tiger is rough.
("tiger" "is" "rough" "+")
int1
The tiger is not kind.
False
1
inv-proof
[(triple2 OR ((triple3 triple4) -> rule4) OR ((triple3 ((triple1) -> rule2)) -> rule4))]
("tiger" "is" "kind" "-")
triple2
((triple3 triple4) -> (rule4 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
((triple3 ((triple1) -> (rule2 % int2))) -> (rule4 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The tiger is rough.
("tiger" "is" "rough" "+")
int2
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 blue.[(triple1)] The tiger is kind.[(triple2 OR ((triple3 triple4) -> rule4) OR ((triple3 ((triple1) -> rule2)) -> rule4))] The tiger is nice.[(triple3)] The tiger is not round.[(triple5)] The tiger is rough.[(triple4 OR ((triple1) -> rule2))]
The tiger is blue.
("tiger" "is" "blue" "+")
triple1
The tiger is kind.
("tiger" "is" "kind" "+")
triple2
((triple3 triple4) -> (rule4 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
((triple3 ((triple1) -> (rule2 % int2))) -> (rule4 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The tiger is rough.
("tiger" "is" "rough" "+")
int2
The tiger is nice.
("tiger" "is" "nice" "+")
triple3
The tiger is not round.
("tiger" "is" "round" "-")
triple5
The tiger is rough.
("tiger" "is" "rough" "+")
triple4
((triple1) -> (rule2 % int1))
The tiger is rough.
("tiger" "is" "rough" "+")
int1