The tiger is not big. The tiger is round. The tiger is young. If the tiger is not round then the tiger is rough. If something is young and blue then it is big. Rough things are big. If something is rough and not round then it is big. Round, rough things are big. Round, young things are not rough. All round, blue things are not rough. All rough, round things are not blue.
The tiger is not big.
("tiger" "is" "big" "-")
The tiger is round.
("tiger" "is" "round" "+")
The tiger is young.
("tiger" "is" "young" "+")
If the tiger is not round then the tiger is rough.
((("tiger" "is" "round" "~")) -> ("tiger" "is" "rough" "+"))
If something is young and blue then it is big.
((("something" "is" "young" "+") ("something" "is" "blue" "+")) -> ("something" "is" "big" "+"))
Rough things are big.
((("something" "is" "rough" "+")) -> ("something" "is" "big" "+"))
If something is rough and not round then it is big.
((("something" "is" "rough" "+") ("something" "is" "round" "~")) -> ("something" "is" "big" "+"))
Round, rough things are big.
((("something" "is" "round" "+") ("something" "is" "rough" "+")) -> ("something" "is" "big" "+"))
Round, young things are not rough.
((("something" "is" "round" "+") ("something" "is" "young" "+")) -> ("something" "is" "rough" "-"))
All round, blue things are not rough.
((("something" "is" "round" "+") ("something" "is" "blue" "+")) -> ("something" "is" "rough" "-"))
All rough, round things are not blue.
((("something" "is" "rough" "+") ("something" "is" "round" "+")) -> ("something" "is" "blue" "-"))
The tiger is not big.
True
1
proof
[(triple1)]
("tiger" "is" "big" "-")
triple1
The tiger is not round.
False
1
inv-proof
[(triple2)]
("tiger" "is" "round" "-")
triple2
The tiger is not rough.
True
3
proof
[(((triple2 triple3) -> rule6))]
("tiger" "is" "rough" "-")
((triple2 triple3) -> (rule6 % int1))
The tiger is not rough.
("tiger" "is" "rough" "-")
int1
The tiger is rough.
False
3
inv-proof
[(((triple2 triple3) -> rule6))]
("tiger" "is" "rough" "+")
((triple2 triple3) -> (rule6 % int1))
The tiger is not rough.
("tiger" "is" "rough" "-")
int1
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 is blue.
Unknown
random
[@0: The tiger is blue.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "blue" "+")
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 likes the tiger.
Unknown
random
[@0: The tiger likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "tiger" "+")
@0: The tiger is not big.[(triple1)] The tiger is round.[(triple2)] The tiger is young.[(triple3)] @1: The tiger is not rough.[(((triple2 triple3) -> rule6))]
The tiger is not big.
("tiger" "is" "big" "-")
triple1
The tiger is round.
("tiger" "is" "round" "+")
triple2
The tiger is young.
("tiger" "is" "young" "+")
triple3
The tiger is not rough.
("tiger" "is" "rough" "-")
((triple2 triple3) -> (rule6 % int1))
The tiger is not rough.
("tiger" "is" "rough" "-")
int1