The tiger is round. If the tiger is round then the tiger is cold. If the tiger is round and the tiger is young then the tiger is cold. If someone is round and kind then they are young. All kind people are young. Cold, red people are young. If someone is kind and not red then they are young. All round people are cold. Round, cold people are kind.
The tiger is round.
("tiger" "is" "round" "+")
If the tiger is round then the tiger is cold.
((("tiger" "is" "round" "+")) -> ("tiger" "is" "cold" "+"))
If the tiger is round and the tiger is young then the tiger is cold.
((("tiger" "is" "round" "+") ("tiger" "is" "young" "+")) -> ("tiger" "is" "cold" "+"))
If someone is round and kind then they are young.
((("someone" "is" "round" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "young" "+"))
All kind people are young.
((("someone" "is" "kind" "+")) -> ("someone" "is" "young" "+"))
Cold, red people are young.
((("someone" "is" "cold" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "young" "+"))
If someone is kind and not red then they are young.
((("someone" "is" "kind" "+") ("someone" "is" "red" "~")) -> ("someone" "is" "young" "+"))
All round people are cold.
((("someone" "is" "round" "+")) -> ("someone" "is" "cold" "+"))
Round, cold people are kind.
((("someone" "is" "round" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "kind" "+"))
The tiger is round.
True
1
proof
[(triple1)]
("tiger" "is" "round" "+")
triple1
The tiger is not round.
False
1
inv-proof
[(triple1)]
("tiger" "is" "round" "-")
triple1
The tiger is cold.
True
2
proof
[(((triple1) -> rule1) OR ((triple1) -> rule7))]
("tiger" "is" "cold" "+")
((triple1) -> (rule1 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
((triple1) -> (rule7 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger is not cold.
False
2
inv-proof
[(((triple1) -> rule1) OR ((triple1) -> rule7))]
("tiger" "is" "cold" "-")
((triple1) -> (rule1 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
((triple1) -> (rule7 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger is kind.
True
4
proof
[(((triple1 ((triple1) -> rule1)) -> rule8) OR ((triple1 ((triple1) -> rule7)) -> rule8))]
("tiger" "is" "kind" "+")
((triple1 ((triple1) -> (rule1 % int2))) -> (rule8 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
int2
((triple1 ((triple1) -> (rule7 % int2))) -> (rule8 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
int2
The tiger is not kind.
False
4
inv-proof
[(((triple1 ((triple1) -> rule1)) -> rule8) OR ((triple1 ((triple1) -> rule7)) -> rule8))]
("tiger" "is" "kind" "-")
((triple1 ((triple1) -> (rule1 % int2))) -> (rule8 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
int2
((triple1 ((triple1) -> (rule7 % int2))) -> (rule8 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
int2
The tiger is not red.
Unknown
inv-random
[@0: The tiger is red.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "red" "-")
The tiger needs the tiger.
Unknown
random
[@0: The tiger needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "tiger" "+")
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 sees the tiger.
Unknown
random
[@0: The tiger sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "tiger" "+")
@0: The tiger is round.[(triple1)] @1: The tiger is cold.[(((triple1) -> rule1) OR ((triple1) -> rule7))] @2: The tiger is kind.[(((triple1 ((triple1) -> rule1)) -> rule8) OR ((triple1 ((triple1) -> rule7)) -> rule8))] @3: The tiger is young.[(((((triple1 ((triple1) -> rule1)) -> rule8)) -> rule4) OR ((((triple1 ((triple1) -> rule7)) -> rule8)) -> rule4) OR ((triple1 ((triple1 ((triple1) -> rule1)) -> rule8)) -> rule3) OR ((triple1 ((triple1 ((triple1) -> rule7)) -> rule8)) -> rule3))]
The tiger is round.
("tiger" "is" "round" "+")
triple1
The tiger is cold.
("tiger" "is" "cold" "+")
((triple1) -> (rule1 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
((triple1) -> (rule7 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger is kind.
("tiger" "is" "kind" "+")
((triple1 ((triple1) -> (rule1 % int2))) -> (rule8 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
int2
((triple1 ((triple1) -> (rule7 % int2))) -> (rule8 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
int2
The tiger is young.
("tiger" "is" "young" "+")
((((triple1 ((triple1) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The tiger is kind.
("tiger" "is" "kind" "+")
int2
The tiger is cold.
("tiger" "is" "cold" "+")
int3
((((triple1 ((triple1) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The tiger is kind.
("tiger" "is" "kind" "+")
int2
The tiger is cold.
("tiger" "is" "cold" "+")
int3
((triple1 ((triple1 ((triple1) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule3 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The tiger is kind.
("tiger" "is" "kind" "+")
int2
The tiger is cold.
("tiger" "is" "cold" "+")
int3
((triple1 ((triple1 ((triple1) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule3 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The tiger is kind.
("tiger" "is" "kind" "+")
int2
The tiger is cold.
("tiger" "is" "cold" "+")
int3