The tiger is kind. If something is nice and young then it is kind. If the tiger is cold then the tiger is young. All kind things are green. All kind, green things are young. If something is cold then it is young. If the tiger is kind then the tiger is green. All kind things are green. If the tiger is cold and the tiger is young then the tiger is nice.
The tiger is kind.
("tiger" "is" "kind" "+")
If something is nice and young then it is kind.
((("something" "is" "nice" "+") ("something" "is" "young" "+")) -> ("something" "is" "kind" "+"))
If the tiger is cold then the tiger is young.
((("tiger" "is" "cold" "+")) -> ("tiger" "is" "young" "+"))
All kind things are green.
((("something" "is" "kind" "+")) -> ("something" "is" "green" "+"))
All kind, green things are young.
((("something" "is" "kind" "+") ("something" "is" "green" "+")) -> ("something" "is" "young" "+"))
If something is cold then it is young.
((("something" "is" "cold" "+")) -> ("something" "is" "young" "+"))
If the tiger is kind then the tiger is green.
((("tiger" "is" "kind" "+")) -> ("tiger" "is" "green" "+"))
All kind things are green.
((("something" "is" "kind" "+")) -> ("something" "is" "green" "+"))
If the tiger is cold and the tiger is young then the tiger is nice.
((("tiger" "is" "cold" "+") ("tiger" "is" "young" "+")) -> ("tiger" "is" "nice" "+"))
The tiger is kind.
True
1
proof
[(triple1)]
("tiger" "is" "kind" "+")
triple1
The tiger is not kind.
False
1
inv-proof
[(triple1)]
("tiger" "is" "kind" "-")
triple1
The tiger is green.
True
2
proof
[(((triple1) -> rule3) OR ((triple1) -> rule6) OR ((triple1) -> rule7))]
("tiger" "is" "green" "+")
((triple1) -> (rule3 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
((triple1) -> (rule6 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
((triple1) -> (rule7 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The tiger is not green.
False
2
inv-proof
[(((triple1) -> rule3) OR ((triple1) -> rule6) OR ((triple1) -> rule7))]
("tiger" "is" "green" "-")
((triple1) -> (rule3 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
((triple1) -> (rule6 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
((triple1) -> (rule7 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The tiger is young.
True
4
proof
[(((triple1 ((triple1) -> rule3)) -> rule4) OR ((triple1 ((triple1) -> rule6)) -> rule4) OR ((triple1 ((triple1) -> rule7)) -> rule4))]
("tiger" "is" "young" "+")
((triple1 ((triple1) -> (rule3 % int2))) -> (rule4 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
int2
((triple1 ((triple1) -> (rule6 % int2))) -> (rule4 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
int2
((triple1 ((triple1) -> (rule7 % int2))) -> (rule4 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
int2
The tiger is not young.
False
4
inv-proof
[(((triple1 ((triple1) -> rule3)) -> rule4) OR ((triple1 ((triple1) -> rule6)) -> rule4) OR ((triple1 ((triple1) -> rule7)) -> rule4))]
("tiger" "is" "young" "-")
((triple1 ((triple1) -> (rule3 % int2))) -> (rule4 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
int2
((triple1 ((triple1) -> (rule6 % int2))) -> (rule4 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
int2
((triple1 ((triple1) -> (rule7 % int2))) -> (rule4 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
int2
The tiger is not nice.
Unknown
inv-rconc
[@1: The tiger is nice.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("tiger" "is" "nice" "-")
The tiger needs the tiger.
Unknown
random
[@0: The tiger needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "tiger" "+")
The tiger is not cold.
Unknown
inv-random
[@0: The tiger is cold.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "cold" "-")
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 kind.[(triple1)] @1: The tiger is green.[(((triple1) -> rule3) OR ((triple1) -> rule6) OR ((triple1) -> rule7))] @2: The tiger is young.[(((triple1 ((triple1) -> rule3)) -> rule4) OR ((triple1 ((triple1) -> rule6)) -> rule4) OR ((triple1 ((triple1) -> rule7)) -> rule4))]
The tiger is kind.
("tiger" "is" "kind" "+")
triple1
The tiger is green.
("tiger" "is" "green" "+")
((triple1) -> (rule3 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
((triple1) -> (rule6 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
((triple1) -> (rule7 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The tiger is young.
("tiger" "is" "young" "+")
((triple1 ((triple1) -> (rule3 % int2))) -> (rule4 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
int2
((triple1 ((triple1) -> (rule6 % int2))) -> (rule4 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
int2
((triple1 ((triple1) -> (rule7 % int2))) -> (rule4 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
int2