The tiger is not blue. The tiger is green. The tiger is kind. The tiger is nice. The tiger is red. Blue, kind people are not green. All blue people are green. All nice, green people are not blue. All blue people are kind. If someone is blue then they are nice. Green people are nice.
The tiger is not blue.
("tiger" "is" "blue" "-")
The tiger is green.
("tiger" "is" "green" "+")
The tiger is kind.
("tiger" "is" "kind" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
The tiger is red.
("tiger" "is" "red" "+")
Blue, kind people are not green.
((("someone" "is" "blue" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "green" "-"))
All blue people are green.
((("someone" "is" "blue" "+")) -> ("someone" "is" "green" "+"))
All nice, green people are not blue.
((("someone" "is" "nice" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "blue" "-"))
All blue people are kind.
((("someone" "is" "blue" "+")) -> ("someone" "is" "kind" "+"))
If someone is blue then they are nice.
((("someone" "is" "blue" "+")) -> ("someone" "is" "nice" "+"))
Green people are nice.
((("someone" "is" "green" "+")) -> ("someone" "is" "nice" "+"))
The tiger is not blue.
True
1
proof
[(triple1 OR ((triple4 triple2) -> rule3) OR ((((triple2) -> rule6) triple2) -> rule3))]
("tiger" "is" "blue" "-")
triple1
((triple4 triple2) -> (rule3 % int1))
The tiger is not blue.
("tiger" "is" "blue" "-")
int1
((((triple2) -> (rule6 % int2)) triple2) -> (rule3 % int1))
The tiger is not blue.
("tiger" "is" "blue" "-")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
int2
The tiger is not red.
False
1
inv-proof
[(triple5)]
("tiger" "is" "red" "-")
triple5
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 sees the tiger.
Unknown
random
[@0: The tiger sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "tiger" "+")
@0: The tiger is green.[(triple2)] The tiger is kind.[(triple3)] The tiger is nice.[(triple4 OR ((triple2) -> rule6))] The tiger is not blue.[(triple1 OR ((triple4 triple2) -> rule3) OR ((((triple2) -> rule6) triple2) -> rule3))] The tiger is red.[(triple5)]
The tiger is green.
("tiger" "is" "green" "+")
triple2
The tiger is kind.
("tiger" "is" "kind" "+")
triple3
The tiger is nice.
("tiger" "is" "nice" "+")
triple4
((triple2) -> (rule6 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
The tiger is not blue.
("tiger" "is" "blue" "-")
triple1
((triple4 triple2) -> (rule3 % int1))
The tiger is not blue.
("tiger" "is" "blue" "-")
int1
((((triple2) -> (rule6 % int2)) triple2) -> (rule3 % int1))
The tiger is not blue.
("tiger" "is" "blue" "-")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
int2
The tiger is red.
("tiger" "is" "red" "+")
triple5