The tiger is nice. Young people are kind. All kind, big people are cold. Kind people are big. Nice people are kind. If someone is young and cold then they are big. All cold people are big.
The tiger is nice.
("tiger" "is" "nice" "+")
Young people are kind.
((("someone" "is" "young" "+")) -> ("someone" "is" "kind" "+"))
All kind, big people are cold.
((("someone" "is" "kind" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "cold" "+"))
Kind people are big.
((("someone" "is" "kind" "+")) -> ("someone" "is" "big" "+"))
Nice people are kind.
((("someone" "is" "nice" "+")) -> ("someone" "is" "kind" "+"))
If someone is young and cold then they are big.
((("someone" "is" "young" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "big" "+"))
All cold people are big.
((("someone" "is" "cold" "+")) -> ("someone" "is" "big" "+"))
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) -> rule4))]
("tiger" "is" "kind" "+")
((triple1) -> (rule4 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The tiger is not kind.
False
2
inv-proof
[(((triple1) -> rule4))]
("tiger" "is" "kind" "-")
((triple1) -> (rule4 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The tiger is big.
True
3
proof
[(((((triple1) -> rule4)) -> rule3))]
("tiger" "is" "big" "+")
((((triple1) -> (rule4 % int2))) -> (rule3 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger is kind.
("tiger" "is" "kind" "+")
int2
The tiger is not big.
False
3
inv-proof
[(((((triple1) -> rule4)) -> rule3))]
("tiger" "is" "big" "-")
((((triple1) -> (rule4 % int2))) -> (rule3 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger is kind.
("tiger" "is" "kind" "+")
int2
The tiger is cold.
True
6
proof
[(((((triple1) -> rule4) ((((triple1) -> rule4)) -> rule3)) -> rule2))]
("tiger" "is" "cold" "+")
((((triple1) -> (rule4 % int3)) ((((triple1) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The tiger is kind.
("tiger" "is" "kind" "+")
int3
The tiger is not cold.
False
6
inv-proof
[(((((triple1) -> rule4) ((((triple1) -> rule4)) -> rule3)) -> rule2))]
("tiger" "is" "cold" "-")
((((triple1) -> (rule4 % int3)) ((((triple1) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
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 is young.
Unknown
random
[@0: The tiger is young.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "young" "+")
The tiger does not need the tiger.
Unknown
inv-random
[@0: The tiger needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "tiger" "-")
The tiger visits the tiger.
Unknown
random
[@0: The tiger visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "tiger" "+")
@0: The tiger is nice.[(triple1)] @1: The tiger is kind.[(((triple1) -> rule4))] @2: The tiger is big.[(((((triple1) -> rule4)) -> rule3))] @3: The tiger is cold.[(((((triple1) -> rule4) ((((triple1) -> rule4)) -> rule3)) -> rule2))]
The tiger is nice.
("tiger" "is" "nice" "+")
triple1
The tiger is kind.
("tiger" "is" "kind" "+")
((triple1) -> (rule4 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
((((triple1) -> (rule4 % int2))) -> (rule3 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger is kind.
("tiger" "is" "kind" "+")
int2
The tiger is cold.
("tiger" "is" "cold" "+")
((((triple1) -> (rule4 % int3)) ((((triple1) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The tiger is kind.
("tiger" "is" "kind" "+")
int3