The tiger is not big. The tiger is blue. The tiger is cold. The tiger is rough. The tiger is not young. Big, cold people are blue. Rough, big people are not blue. Cold, rough people are blue. If the tiger is young and the tiger is big then the tiger is not blue. All blue people are not young. If someone is rough then they are cold. All young people are cold. Young, blue people are rough.
The tiger is not big.
("tiger" "is" "big" "-")
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
The tiger is not young.
("tiger" "is" "young" "-")
Big, cold people are blue.
((("someone" "is" "big" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "blue" "+"))
Rough, big people are not blue.
((("someone" "is" "rough" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "blue" "-"))
Cold, rough people are blue.
((("someone" "is" "cold" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "blue" "+"))
If the tiger is young and the tiger is big then the tiger is not blue.
((("tiger" "is" "young" "+") ("tiger" "is" "big" "+")) -> ("tiger" "is" "blue" "-"))
All blue people are not young.
((("someone" "is" "blue" "+")) -> ("someone" "is" "young" "-"))
If someone is rough then they are cold.
((("someone" "is" "rough" "+")) -> ("someone" "is" "cold" "+"))
All young people are cold.
((("someone" "is" "young" "+")) -> ("someone" "is" "cold" "+"))
Young, blue people are rough.
((("someone" "is" "young" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "rough" "+"))
The tiger is cold.
True
1
proof
[(triple3 OR ((triple4) -> rule6))]
("tiger" "is" "cold" "+")
triple3
((triple4) -> (rule6 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger is not rough.
False
1
inv-proof
[(triple4)]
("tiger" "is" "rough" "-")
triple4
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 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.[(triple2 OR ((triple3 triple4) -> rule3) OR ((((triple4) -> rule6) triple4) -> rule3))] The tiger is cold.[(triple3 OR ((triple4) -> rule6))] The tiger is not big.[(triple1)] The tiger is not young.[(triple5 OR ((triple2) -> rule5) OR ((((triple3 triple4) -> rule3)) -> rule5) OR ((((((triple4) -> rule6) triple4) -> rule3)) -> rule5))] The tiger is rough.[(triple4)]
The tiger is blue.
("tiger" "is" "blue" "+")
triple2
((triple3 triple4) -> (rule3 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
((((triple4) -> (rule6 % int2)) triple4) -> (rule3 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
int2
The tiger is cold.
("tiger" "is" "cold" "+")
triple3
((triple4) -> (rule6 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger is not big.
("tiger" "is" "big" "-")
triple1
The tiger is not young.
("tiger" "is" "young" "-")
triple5
((triple2) -> (rule5 % int1))
The tiger is not young.
("tiger" "is" "young" "-")
int1
((((triple3 triple4) -> (rule3 % int2))) -> (rule5 % int1))
The tiger is not young.
("tiger" "is" "young" "-")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
int2
((((((triple4) -> (rule6 % int3)) triple4) -> (rule3 % int2))) -> (rule5 % int1))
The tiger is not young.
("tiger" "is" "young" "-")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
int2
The tiger is cold.
("tiger" "is" "cold" "+")
int3
The tiger is rough.
("tiger" "is" "rough" "+")
triple4