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