The tiger is kind. If the tiger is green and the tiger is kind then the tiger is rough. Nice things are green. If something is kind then it is nice.
The tiger is kind.
("tiger" "is" "kind" "+")
If the tiger is green and the tiger is kind then the tiger is rough.
((("tiger" "is" "green" "+") ("tiger" "is" "kind" "+")) -> ("tiger" "is" "rough" "+"))
Nice things are green.
((("something" "is" "nice" "+")) -> ("something" "is" "green" "+"))
If something is kind then it is nice.
((("something" "is" "kind" "+")) -> ("something" "is" "nice" "+"))
The tiger is kind.
True
1
proof
[(triple1)]
("tiger" "is" "kind" "+")
triple1
The tiger is not kind.
False
1
inv-proof
[(triple1)]
("tiger" "is" "kind" "-")
triple1
The tiger is nice.
True
2
proof
[(((triple1) -> rule3))]
("tiger" "is" "nice" "+")
((triple1) -> (rule3 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
The tiger is not nice.
False
2
inv-proof
[(((triple1) -> rule3))]
("tiger" "is" "nice" "-")
((triple1) -> (rule3 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
The tiger is green.
True
3
proof
[(((((triple1) -> rule3)) -> rule2))]
("tiger" "is" "green" "+")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
int2
The tiger is not green.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule2))]
("tiger" "is" "green" "-")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
int2
The tiger is rough.
True
5
proof
[(((((((triple1) -> rule3)) -> rule2) triple1) -> rule1))]
("tiger" "is" "rough" "+")
((((((triple1) -> (rule3 % int3))) -> (rule2 % int2)) triple1) -> (rule1 % int1))
The tiger is rough.
("tiger" "is" "rough" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
int2
The tiger is nice.
("tiger" "is" "nice" "+")
int3
The tiger is not rough.
False
5
inv-proof
[(((((((triple1) -> rule3)) -> rule2) triple1) -> rule1))]
("tiger" "is" "rough" "-")
((((((triple1) -> (rule3 % int3))) -> (rule2 % int2)) triple1) -> (rule1 % int1))
The tiger is rough.
("tiger" "is" "rough" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
int2
The tiger is nice.
("tiger" "is" "nice" "+")
int3
The tiger does not like the tiger.
Unknown
inv-random
[@0: The tiger likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "tiger" "-")
The tiger is round.
Unknown
random
[@0: The tiger is round.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "round" "+")
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 chases the tiger.
Unknown
random
[@0: The tiger chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "tiger" "+")
@0: The tiger is kind.[(triple1)] @1: The tiger is nice.[(((triple1) -> rule3))] @2: The tiger is green.[(((((triple1) -> rule3)) -> rule2))] @3: The tiger is rough.[(((((((triple1) -> rule3)) -> rule2) triple1) -> rule1))]
The tiger is kind.
("tiger" "is" "kind" "+")
triple1
The tiger is nice.
("tiger" "is" "nice" "+")
((triple1) -> (rule3 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
int2
The tiger is rough.
("tiger" "is" "rough" "+")
((((((triple1) -> (rule3 % int3))) -> (rule2 % int2)) triple1) -> (rule1 % int1))
The tiger is rough.
("tiger" "is" "rough" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
int2
The tiger is nice.
("tiger" "is" "nice" "+")
int3