The tiger is green. Kind, green people are blue. All green, blue people are nice. If the tiger is green then the tiger is kind.
The tiger is green.
("tiger" "is" "green" "+")
Kind, green people are blue.
((("someone" "is" "kind" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "blue" "+"))
All green, blue people are nice.
((("someone" "is" "green" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "nice" "+"))
If the tiger is green then the tiger is kind.
((("tiger" "is" "green" "+")) -> ("tiger" "is" "kind" "+"))
The tiger is green.
True
1
proof
[(triple1)]
("tiger" "is" "green" "+")
triple1
The tiger is not green.
False
1
inv-proof
[(triple1)]
("tiger" "is" "green" "-")
triple1
The tiger is kind.
True
2
proof
[(((triple1) -> rule3))]
("tiger" "is" "kind" "+")
((triple1) -> (rule3 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The tiger is not kind.
False
2
inv-proof
[(((triple1) -> rule3))]
("tiger" "is" "kind" "-")
((triple1) -> (rule3 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The tiger is blue.
True
4
proof
[(((((triple1) -> rule3) triple1) -> rule1))]
("tiger" "is" "blue" "+")
((((triple1) -> (rule3 % int2)) triple1) -> (rule1 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The tiger is kind.
("tiger" "is" "kind" "+")
int2
The tiger is not blue.
False
4
inv-proof
[(((((triple1) -> rule3) triple1) -> rule1))]
("tiger" "is" "blue" "-")
((((triple1) -> (rule3 % int2)) triple1) -> (rule1 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The tiger is kind.
("tiger" "is" "kind" "+")
int2
The tiger is nice.
True
6
proof
[(((triple1 ((((triple1) -> rule3) triple1) -> rule1)) -> rule2))]
("tiger" "is" "nice" "+")
((triple1 ((((triple1) -> (rule3 % int3)) triple1) -> (rule1 % int2))) -> (rule2 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
int2
The tiger is kind.
("tiger" "is" "kind" "+")
int3
The tiger is not nice.
False
6
inv-proof
[(((triple1 ((((triple1) -> rule3) triple1) -> rule1)) -> rule2))]
("tiger" "is" "nice" "-")
((triple1 ((((triple1) -> (rule3 % int3)) triple1) -> (rule1 % int2))) -> (rule2 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
int2
The tiger is kind.
("tiger" "is" "kind" "+")
int3
The tiger does not eat the tiger.
Unknown
inv-random
[@0: The tiger eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "tiger" "-")
The tiger visits the tiger.
Unknown
random
[@0: The tiger visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "tiger" "+")
The tiger is not round.
Unknown
inv-random
[@0: The tiger is round.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "round" "-")
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 green.[(triple1)] @1: The tiger is kind.[(((triple1) -> rule3))] @2: The tiger is blue.[(((((triple1) -> rule3) triple1) -> rule1))] @3: The tiger is nice.[(((triple1 ((((triple1) -> rule3) triple1) -> rule1)) -> rule2))]
The tiger is green.
("tiger" "is" "green" "+")
triple1
The tiger is kind.
("tiger" "is" "kind" "+")
((triple1) -> (rule3 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
((((triple1) -> (rule3 % int2)) triple1) -> (rule1 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The tiger is kind.
("tiger" "is" "kind" "+")
int2
The tiger is nice.
("tiger" "is" "nice" "+")
((triple1 ((((triple1) -> (rule3 % int3)) triple1) -> (rule1 % int2))) -> (rule2 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
int2
The tiger is kind.
("tiger" "is" "kind" "+")
int3