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