The tiger is big. The tiger is green. The tiger is rough. If the tiger is rough and the tiger is nice then the tiger is cold. All cold, big people are nice. Nice people are green. If the tiger is rough then the tiger is green. All rough people are cold. Cold, nice people are big.
The tiger is big.
("tiger" "is" "big" "+")
The tiger is green.
("tiger" "is" "green" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
If the tiger is rough and the tiger is nice then the tiger is cold.
((("tiger" "is" "rough" "+") ("tiger" "is" "nice" "+")) -> ("tiger" "is" "cold" "+"))
All cold, big people are nice.
((("someone" "is" "cold" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "nice" "+"))
Nice people are green.
((("someone" "is" "nice" "+")) -> ("someone" "is" "green" "+"))
If the tiger is rough then the tiger is green.
((("tiger" "is" "rough" "+")) -> ("tiger" "is" "green" "+"))
All rough people are cold.
((("someone" "is" "rough" "+")) -> ("someone" "is" "cold" "+"))
Cold, nice people are big.
((("someone" "is" "cold" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "big" "+"))
The tiger is green.
True
1
proof
[(triple2 OR ((triple3) -> rule4) OR ((((((triple3) -> rule5) triple1) -> rule2)) -> rule3))]
("tiger" "is" "green" "+")
triple2
((triple3) -> (rule4 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
((((((triple3) -> (rule5 % int3)) triple1) -> (rule2 % int2))) -> (rule3 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
int2
The tiger is cold.
("tiger" "is" "cold" "+")
int3
The tiger is not big.
False
1
inv-proof
[(triple1)]
("tiger" "is" "big" "-")
triple1
The tiger is cold.
True
2
proof
[(((triple3) -> rule5))]
("tiger" "is" "cold" "+")
((triple3) -> (rule5 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger is not cold.
False
2
inv-proof
[(((triple3) -> rule5))]
("tiger" "is" "cold" "-")
((triple3) -> (rule5 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger is nice.
True
4
proof
[(((((triple3) -> rule5) triple1) -> rule2))]
("tiger" "is" "nice" "+")
((((triple3) -> (rule5 % int2)) triple1) -> (rule2 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
int2
The tiger is not nice.
False
4
inv-proof
[(((((triple3) -> rule5) triple1) -> rule2))]
("tiger" "is" "nice" "-")
((((triple3) -> (rule5 % int2)) triple1) -> (rule2 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
int2
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 eats the tiger.
Unknown
random
[@0: The tiger eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "tiger" "+")
@0: The tiger is big.[(triple1)] The tiger is green.[(triple2 OR ((triple3) -> rule4) OR ((((((triple3) -> rule5) triple1) -> rule2)) -> rule3))] The tiger is rough.[(triple3)] @1: The tiger is cold.[(((triple3) -> rule5))] @2: The tiger is nice.[(((((triple3) -> rule5) triple1) -> rule2))]
The tiger is big.
("tiger" "is" "big" "+")
triple1
The tiger is green.
("tiger" "is" "green" "+")
triple2
((triple3) -> (rule4 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
((((((triple3) -> (rule5 % int3)) triple1) -> (rule2 % int2))) -> (rule3 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
int2
The tiger is cold.
("tiger" "is" "cold" "+")
int3
The tiger is rough.
("tiger" "is" "rough" "+")
triple3
The tiger is cold.
("tiger" "is" "cold" "+")
((triple3) -> (rule5 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
((((triple3) -> (rule5 % int2)) triple1) -> (rule2 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
int2