The tiger is nice. Big, red people are kind. If someone is nice then they are kind. All red people are big. If someone is red then they are big. All kind, nice people are red. If the tiger is nice then the tiger is round.
The tiger is nice.
("tiger" "is" "nice" "+")
Big, red people are kind.
((("someone" "is" "big" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "kind" "+"))
If someone is nice then they are kind.
((("someone" "is" "nice" "+")) -> ("someone" "is" "kind" "+"))
All red people are big.
((("someone" "is" "red" "+")) -> ("someone" "is" "big" "+"))
If someone is red then they are big.
((("someone" "is" "red" "+")) -> ("someone" "is" "big" "+"))
All kind, nice people are red.
((("someone" "is" "kind" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "red" "+"))
If the tiger is nice then the tiger is round.
((("tiger" "is" "nice" "+")) -> ("tiger" "is" "round" "+"))
The tiger is nice.
True
1
proof
[(triple1)]
("tiger" "is" "nice" "+")
triple1
The tiger is not nice.
False
1
inv-proof
[(triple1)]
("tiger" "is" "nice" "-")
triple1
The tiger is kind.
True
2
proof
[(((triple1) -> rule2))]
("tiger" "is" "kind" "+")
((triple1) -> (rule2 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The tiger is not round.
False
2
inv-proof
[(((triple1) -> rule6))]
("tiger" "is" "round" "-")
((triple1) -> (rule6 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The tiger is red.
True
4
proof
[(((((triple1) -> rule2) triple1) -> rule5))]
("tiger" "is" "red" "+")
((((triple1) -> (rule2 % int2)) triple1) -> (rule5 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
The tiger is kind.
("tiger" "is" "kind" "+")
int2
The tiger is not red.
False
4
inv-proof
[(((((triple1) -> rule2) triple1) -> rule5))]
("tiger" "is" "red" "-")
((((triple1) -> (rule2 % int2)) triple1) -> (rule5 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
The tiger is kind.
("tiger" "is" "kind" "+")
int2
The tiger is big.
True
5
proof
[(((((((triple1) -> rule2) triple1) -> rule5)) -> rule3) OR ((((((triple1) -> rule2) triple1) -> rule5)) -> rule4))]
("tiger" "is" "big" "+")
((((((triple1) -> (rule2 % int3)) triple1) -> (rule5 % int2))) -> (rule3 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger is red.
("tiger" "is" "red" "+")
int2
The tiger is kind.
("tiger" "is" "kind" "+")
int3
((((((triple1) -> (rule2 % int3)) triple1) -> (rule5 % int2))) -> (rule4 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger is red.
("tiger" "is" "red" "+")
int2
The tiger is kind.
("tiger" "is" "kind" "+")
int3
The tiger is not big.
False
5
inv-proof
[(((((((triple1) -> rule2) triple1) -> rule5)) -> rule3) OR ((((((triple1) -> rule2) triple1) -> rule5)) -> rule4))]
("tiger" "is" "big" "-")
((((((triple1) -> (rule2 % int3)) triple1) -> (rule5 % int2))) -> (rule3 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger is red.
("tiger" "is" "red" "+")
int2
The tiger is kind.
("tiger" "is" "kind" "+")
int3
((((((triple1) -> (rule2 % int3)) triple1) -> (rule5 % int2))) -> (rule4 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger is red.
("tiger" "is" "red" "+")
int2
The tiger is kind.
("tiger" "is" "kind" "+")
int3
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 nice.[(triple1)] @1: The tiger is kind.[(((triple1) -> rule2))] The tiger is round.[(((triple1) -> rule6))] @2: The tiger is red.[(((((triple1) -> rule2) triple1) -> rule5))] @3: The tiger is big.[(((((((triple1) -> rule2) triple1) -> rule5)) -> rule3) OR ((((((triple1) -> rule2) triple1) -> rule5)) -> rule4))]
The tiger is nice.
("tiger" "is" "nice" "+")
triple1
The tiger is kind.
("tiger" "is" "kind" "+")
((triple1) -> (rule2 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The tiger is round.
("tiger" "is" "round" "+")
((triple1) -> (rule6 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The tiger is red.
("tiger" "is" "red" "+")
((((triple1) -> (rule2 % int2)) triple1) -> (rule5 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
The tiger is kind.
("tiger" "is" "kind" "+")
int2
The tiger is big.
("tiger" "is" "big" "+")
((((((triple1) -> (rule2 % int3)) triple1) -> (rule5 % int2))) -> (rule3 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger is red.
("tiger" "is" "red" "+")
int2
The tiger is kind.
("tiger" "is" "kind" "+")
int3
((((((triple1) -> (rule2 % int3)) triple1) -> (rule5 % int2))) -> (rule4 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger is red.
("tiger" "is" "red" "+")
int2
The tiger is kind.
("tiger" "is" "kind" "+")
int3