The tiger is big. The tiger is green. The tiger is young. All rough things are not round. If the tiger is big and the tiger is young then the tiger is rough. If something is young and not green then it is big.
The tiger is big.
("tiger" "is" "big" "+")
The tiger is green.
("tiger" "is" "green" "+")
The tiger is young.
("tiger" "is" "young" "+")
All rough things are not round.
((("something" "is" "rough" "+")) -> ("something" "is" "round" "-"))
If the tiger is big and the tiger is young then the tiger is rough.
((("tiger" "is" "big" "+") ("tiger" "is" "young" "+")) -> ("tiger" "is" "rough" "+"))
If something is young and not green then it is big.
((("something" "is" "young" "+") ("something" "is" "green" "~")) -> ("something" "is" "big" "+"))
The tiger is green.
True
1
proof
[(triple2)]
("tiger" "is" "green" "+")
triple2
The tiger is not green.
False
1
inv-proof
[(triple2)]
("tiger" "is" "green" "-")
triple2
The tiger is rough.
True
3
proof
[(((triple1 triple3) -> rule2))]
("tiger" "is" "rough" "+")
((triple1 triple3) -> (rule2 % int1))
The tiger is rough.
("tiger" "is" "rough" "+")
int1
The tiger is not rough.
False
3
inv-proof
[(((triple1 triple3) -> rule2))]
("tiger" "is" "rough" "-")
((triple1 triple3) -> (rule2 % int1))
The tiger is rough.
("tiger" "is" "rough" "+")
int1
The tiger is not round.
True
4
proof
[(((((triple1 triple3) -> rule2)) -> rule1))]
("tiger" "is" "round" "-")
((((triple1 triple3) -> (rule2 % int2))) -> (rule1 % int1))
The tiger is not round.
("tiger" "is" "round" "-")
int1
The tiger is rough.
("tiger" "is" "rough" "+")
int2
The tiger is round.
False
4
inv-proof
[(((((triple1 triple3) -> rule2)) -> rule1))]
("tiger" "is" "round" "+")
((((triple1 triple3) -> (rule2 % int2))) -> (rule1 % int1))
The tiger is not round.
("tiger" "is" "round" "-")
int1
The tiger is rough.
("tiger" "is" "rough" "+")
int2
The tiger does not see the tiger.
Unknown
inv-random
[@0: The tiger sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "tiger" "-")
The tiger chases the tiger.
Unknown
random
[@0: The tiger chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "tiger" "+")
@0: The tiger is big.[(triple1)] The tiger is green.[(triple2)] The tiger is young.[(triple3)] @1: The tiger is rough.[(((triple1 triple3) -> rule2))] @2: The tiger is not round.[(((((triple1 triple3) -> rule2)) -> rule1))]
The tiger is big.
("tiger" "is" "big" "+")
triple1
The tiger is green.
("tiger" "is" "green" "+")
triple2
The tiger is young.
("tiger" "is" "young" "+")
triple3
The tiger is rough.
("tiger" "is" "rough" "+")
((triple1 triple3) -> (rule2 % int1))
The tiger is rough.
("tiger" "is" "rough" "+")
int1
The tiger is not round.
("tiger" "is" "round" "-")
((((triple1 triple3) -> (rule2 % int2))) -> (rule1 % int1))
The tiger is not round.
("tiger" "is" "round" "-")
int1
The tiger is rough.
("tiger" "is" "rough" "+")
int2