The tiger is cold. If something is kind then it is nice. If something is round then it is cold. If the tiger is cold and the tiger is round then the tiger is not nice. If something is nice and not kind then it is not round. If the tiger is cold then the tiger is round. If the tiger is not cold then the tiger is young.
The tiger is cold.
("tiger" "is" "cold" "+")
If something is kind then it is nice.
((("something" "is" "kind" "+")) -> ("something" "is" "nice" "+"))
If something is round then it is cold.
((("something" "is" "round" "+")) -> ("something" "is" "cold" "+"))
If the tiger is cold and the tiger is round then the tiger is not nice.
((("tiger" "is" "cold" "+") ("tiger" "is" "round" "+")) -> ("tiger" "is" "nice" "-"))
If something is nice and not kind then it is not round.
((("something" "is" "nice" "+") ("something" "is" "kind" "~")) -> ("something" "is" "round" "-"))
If the tiger is cold then the tiger is round.
((("tiger" "is" "cold" "+")) -> ("tiger" "is" "round" "+"))
If the tiger is not cold then the tiger is young.
((("tiger" "is" "cold" "~")) -> ("tiger" "is" "young" "+"))
The tiger is cold.
True
1
proof
[(triple1)]
("tiger" "is" "cold" "+")
triple1
The tiger is not cold.
False
1
inv-proof
[(triple1)]
("tiger" "is" "cold" "-")
triple1
The tiger is round.
True
2
proof
[(((triple1) -> rule5))]
("tiger" "is" "round" "+")
((triple1) -> (rule5 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The tiger is not round.
False
2
inv-proof
[(((triple1) -> rule5))]
("tiger" "is" "round" "-")
((triple1) -> (rule5 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The tiger is not nice.
True
4
proof
[(((triple1 ((triple1) -> rule5)) -> rule3))]
("tiger" "is" "nice" "-")
((triple1 ((triple1) -> (rule5 % int2))) -> (rule3 % int1))
The tiger is not nice.
("tiger" "is" "nice" "-")
int1
The tiger is round.
("tiger" "is" "round" "+")
int2
The tiger is nice.
False
4
inv-proof
[(((triple1 ((triple1) -> rule5)) -> rule3))]
("tiger" "is" "nice" "+")
((triple1 ((triple1) -> (rule5 % int2))) -> (rule3 % int1))
The tiger is not nice.
("tiger" "is" "nice" "-")
int1
The tiger is round.
("tiger" "is" "round" "+")
int2
The tiger is not young.
Unknown
inv-rconc
[@1: The tiger is young.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("tiger" "is" "young" "-")
The tiger eats the tiger.
Unknown
random
[@0: The tiger eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "tiger" "+")
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 sees the tiger.
Unknown
random
[@0: The tiger sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "tiger" "+")
@0: The tiger is cold.[(triple1)] @1: The tiger is round.[(((triple1) -> rule5))] @2: The tiger is not nice.[(((triple1 ((triple1) -> rule5)) -> rule3))]
The tiger is cold.
("tiger" "is" "cold" "+")
triple1
The tiger is round.
("tiger" "is" "round" "+")
((triple1) -> (rule5 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The tiger is not nice.
("tiger" "is" "nice" "-")
((triple1 ((triple1) -> (rule5 % int2))) -> (rule3 % int1))
The tiger is not nice.
("tiger" "is" "nice" "-")
int1
The tiger is round.
("tiger" "is" "round" "+")
int2