The tiger is big. The tiger is nice. The tiger is rough. All red, rough things are not big. If the tiger is big then the tiger is not red. All big things are not red. If something is red then it is not nice. If something is rough and not red then it is nice. If the tiger is rough and the tiger is not big then the tiger is not nice. If the tiger is red then the tiger is not nice. If something is rough and not red then it is not cold.
The tiger is big.
("tiger" "is" "big" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
All red, rough things are not big.
((("something" "is" "red" "+") ("something" "is" "rough" "+")) -> ("something" "is" "big" "-"))
If the tiger is big then the tiger is not red.
((("tiger" "is" "big" "+")) -> ("tiger" "is" "red" "-"))
All big things are not red.
((("something" "is" "big" "+")) -> ("something" "is" "red" "-"))
If something is red then it is not nice.
((("something" "is" "red" "+")) -> ("something" "is" "nice" "-"))
If something is rough and not red then it is nice.
((("something" "is" "rough" "+") ("something" "is" "red" "~")) -> ("something" "is" "nice" "+"))
If the tiger is rough and the tiger is not big then the tiger is not nice.
((("tiger" "is" "rough" "+") ("tiger" "is" "big" "~")) -> ("tiger" "is" "nice" "-"))
If the tiger is red then the tiger is not nice.
((("tiger" "is" "red" "+")) -> ("tiger" "is" "nice" "-"))
If something is rough and not red then it is not cold.
((("something" "is" "rough" "+") ("something" "is" "red" "~")) -> ("something" "is" "cold" "-"))
The tiger is big.
True
1
proof
[(triple1)]
("tiger" "is" "big" "+")
triple1
The tiger is not big.
False
1
inv-proof
[(triple1)]
("tiger" "is" "big" "-")
triple1
The tiger is not red.
True
2
proof
[(((triple1) -> rule2) OR ((triple1) -> rule3))]
("tiger" "is" "red" "-")
((triple1) -> (rule2 % int1))
The tiger is not red.
("tiger" "is" "red" "-")
int1
((triple1) -> (rule3 % int1))
The tiger is not red.
("tiger" "is" "red" "-")
int1
The tiger is red.
False
2
inv-proof
[(((triple1) -> rule2) OR ((triple1) -> rule3))]
("tiger" "is" "red" "+")
((triple1) -> (rule2 % int1))
The tiger is not red.
("tiger" "is" "red" "-")
int1
((triple1) -> (rule3 % int1))
The tiger is not red.
("tiger" "is" "red" "-")
int1
The tiger is not cold.
True
4
proof
[(((triple3 ((triple1) -> rule2)) -> rule8) OR ((triple3 ((triple1) -> rule3)) -> rule8))]
("tiger" "is" "cold" "-")
((triple3 ((triple1) -> (rule2 % int2))) -> (rule8 % int1))
The tiger is not cold.
("tiger" "is" "cold" "-")
int1
The tiger is not red.
("tiger" "is" "red" "-")
int2
((triple3 ((triple1) -> (rule3 % int2))) -> (rule8 % int1))
The tiger is not cold.
("tiger" "is" "cold" "-")
int1
The tiger is not red.
("tiger" "is" "red" "-")
int2
The tiger is cold.
False
4
inv-proof
[(((triple3 ((triple1) -> rule2)) -> rule8) OR ((triple3 ((triple1) -> rule3)) -> rule8))]
("tiger" "is" "cold" "+")
((triple3 ((triple1) -> (rule2 % int2))) -> (rule8 % int1))
The tiger is not cold.
("tiger" "is" "cold" "-")
int1
The tiger is not red.
("tiger" "is" "red" "-")
int2
((triple3 ((triple1) -> (rule3 % int2))) -> (rule8 % int1))
The tiger is not cold.
("tiger" "is" "cold" "-")
int1
The tiger is not red.
("tiger" "is" "red" "-")
int2
The tiger does not need the tiger.
Unknown
inv-random
[@0: The tiger needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "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 big.[(triple1)] The tiger is nice.[(triple2 OR ((triple3 ((triple1) -> rule2)) -> rule5) OR ((triple3 ((triple1) -> rule3)) -> rule5))] The tiger is rough.[(triple3)] @1: The tiger is not red.[(((triple1) -> rule2) OR ((triple1) -> rule3))] @2: The tiger is not cold.[(((triple3 ((triple1) -> rule2)) -> rule8) OR ((triple3 ((triple1) -> rule3)) -> rule8))]
The tiger is big.
("tiger" "is" "big" "+")
triple1
The tiger is nice.
("tiger" "is" "nice" "+")
triple2
((triple3 ((triple1) -> (rule2 % int2))) -> (rule5 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
The tiger is not red.
("tiger" "is" "red" "-")
int2
((triple3 ((triple1) -> (rule3 % int2))) -> (rule5 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
The tiger is not red.
("tiger" "is" "red" "-")
int2
The tiger is rough.
("tiger" "is" "rough" "+")
triple3
The tiger is not red.
("tiger" "is" "red" "-")
((triple1) -> (rule2 % int1))
The tiger is not red.
("tiger" "is" "red" "-")
int1
((triple1) -> (rule3 % int1))
The tiger is not red.
("tiger" "is" "red" "-")
int1
The tiger is not cold.
("tiger" "is" "cold" "-")
((triple3 ((triple1) -> (rule2 % int2))) -> (rule8 % int1))
The tiger is not cold.
("tiger" "is" "cold" "-")
int1
The tiger is not red.
("tiger" "is" "red" "-")
int2
((triple3 ((triple1) -> (rule3 % int2))) -> (rule8 % int1))
The tiger is not cold.
("tiger" "is" "cold" "-")
int1
The tiger is not red.
("tiger" "is" "red" "-")
int2