The cat is kind. If something is cold and kind then it is young. All kind things are cold. If something is kind and red then it is big. If the cat is kind then the cat is cold. Kind things are young. Big things are red. If something is kind and big then it is young. If something is young then it is red.
The cat is kind.
("cat" "is" "kind" "+")
If something is cold and kind then it is young.
((("something" "is" "cold" "+") ("something" "is" "kind" "+")) -> ("something" "is" "young" "+"))
All kind things are cold.
((("something" "is" "kind" "+")) -> ("something" "is" "cold" "+"))
If something is kind and red then it is big.
((("something" "is" "kind" "+") ("something" "is" "red" "+")) -> ("something" "is" "big" "+"))
If the cat is kind then the cat is cold.
((("cat" "is" "kind" "+")) -> ("cat" "is" "cold" "+"))
Kind things are young.
((("something" "is" "kind" "+")) -> ("something" "is" "young" "+"))
Big things are red.
((("something" "is" "big" "+")) -> ("something" "is" "red" "+"))
If something is kind and big then it is young.
((("something" "is" "kind" "+") ("something" "is" "big" "+")) -> ("something" "is" "young" "+"))
If something is young then it is red.
((("something" "is" "young" "+")) -> ("something" "is" "red" "+"))
The cat is kind.
True
1
proof
[(triple1)]
("cat" "is" "kind" "+")
triple1
The cat is not kind.
False
1
inv-proof
[(triple1)]
("cat" "is" "kind" "-")
triple1
The cat is cold.
True
2
proof
[(((triple1) -> rule2) OR ((triple1) -> rule4))]
("cat" "is" "cold" "+")
((triple1) -> (rule2 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
((triple1) -> (rule4 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
The cat is not cold.
False
2
inv-proof
[(((triple1) -> rule2) OR ((triple1) -> rule4))]
("cat" "is" "cold" "-")
((triple1) -> (rule2 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
((triple1) -> (rule4 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
The cat is red.
True
3
proof
[(((((triple1) -> rule5)) -> rule8) OR ((((((triple1) -> rule2) triple1) -> rule1)) -> rule8) OR ((((((triple1) -> rule4) triple1) -> rule1)) -> rule8))]
("cat" "is" "red" "+")
((((triple1) -> (rule5 % int2))) -> (rule8 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat is young.
("cat" "is" "young" "+")
int2
((((((triple1) -> (rule2 % int3)) triple1) -> (rule1 % int2))) -> (rule8 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat is young.
("cat" "is" "young" "+")
int2
The cat is cold.
("cat" "is" "cold" "+")
int3
((((((triple1) -> (rule4 % int3)) triple1) -> (rule1 % int2))) -> (rule8 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat is young.
("cat" "is" "young" "+")
int2
The cat is cold.
("cat" "is" "cold" "+")
int3
The cat is not red.
False
3
inv-proof
[(((((triple1) -> rule5)) -> rule8) OR ((((((triple1) -> rule2) triple1) -> rule1)) -> rule8) OR ((((((triple1) -> rule4) triple1) -> rule1)) -> rule8))]
("cat" "is" "red" "-")
((((triple1) -> (rule5 % int2))) -> (rule8 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat is young.
("cat" "is" "young" "+")
int2
((((((triple1) -> (rule2 % int3)) triple1) -> (rule1 % int2))) -> (rule8 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat is young.
("cat" "is" "young" "+")
int2
The cat is cold.
("cat" "is" "cold" "+")
int3
((((((triple1) -> (rule4 % int3)) triple1) -> (rule1 % int2))) -> (rule8 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat is young.
("cat" "is" "young" "+")
int2
The cat is cold.
("cat" "is" "cold" "+")
int3
The cat is big.
True
5
proof
[(((triple1 ((((triple1) -> rule5)) -> rule8)) -> rule3) OR ((triple1 ((((((triple1) -> rule2) triple1) -> rule1)) -> rule8)) -> rule3) OR ((triple1 ((((((triple1) -> rule4) triple1) -> rule1)) -> rule8)) -> rule3))]
("cat" "is" "big" "+")
((triple1 ((((triple1) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule3 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2
The cat is young.
("cat" "is" "young" "+")
int3
((triple1 ((((((triple1) -> (rule2 % int4)) triple1) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule3 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2
The cat is young.
("cat" "is" "young" "+")
int3
The cat is cold.
("cat" "is" "cold" "+")
int4
((triple1 ((((((triple1) -> (rule4 % int4)) triple1) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule3 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2
The cat is young.
("cat" "is" "young" "+")
int3
The cat is cold.
("cat" "is" "cold" "+")
int4
The cat is not big.
False
5
inv-proof
[(((triple1 ((((triple1) -> rule5)) -> rule8)) -> rule3) OR ((triple1 ((((((triple1) -> rule2) triple1) -> rule1)) -> rule8)) -> rule3) OR ((triple1 ((((((triple1) -> rule4) triple1) -> rule1)) -> rule8)) -> rule3))]
("cat" "is" "big" "-")
((triple1 ((((triple1) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule3 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2
The cat is young.
("cat" "is" "young" "+")
int3
((triple1 ((((((triple1) -> (rule2 % int4)) triple1) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule3 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2
The cat is young.
("cat" "is" "young" "+")
int3
The cat is cold.
("cat" "is" "cold" "+")
int4
((triple1 ((((((triple1) -> (rule4 % int4)) triple1) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule3 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2
The cat is young.
("cat" "is" "young" "+")
int3
The cat is cold.
("cat" "is" "cold" "+")
int4
The cat does not need the cat.
Unknown
inv-random
[@0: The cat needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "cat" "-")
The cat likes the cat.
Unknown
random
[@0: The cat likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "cat" "+")
@0: The cat is kind.[(triple1)] @1: The cat is cold.[(((triple1) -> rule2) OR ((triple1) -> rule4))] The cat is young.[(((triple1) -> rule5) OR ((((triple1) -> rule2) triple1) -> rule1) OR ((((triple1) -> rule4) triple1) -> rule1))] @2: The cat is red.[(((((triple1) -> rule5)) -> rule8) OR ((((((triple1) -> rule2) triple1) -> rule1)) -> rule8) OR ((((((triple1) -> rule4) triple1) -> rule1)) -> rule8))] @3: The cat is big.[(((triple1 ((((triple1) -> rule5)) -> rule8)) -> rule3) OR ((triple1 ((((((triple1) -> rule2) triple1) -> rule1)) -> rule8)) -> rule3) OR ((triple1 ((((((triple1) -> rule4) triple1) -> rule1)) -> rule8)) -> rule3))]
The cat is kind.
("cat" "is" "kind" "+")
triple1
The cat is cold.
("cat" "is" "cold" "+")
((triple1) -> (rule2 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
((triple1) -> (rule4 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
The cat is young.
("cat" "is" "young" "+")
((triple1) -> (rule5 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
((((triple1) -> (rule2 % int2)) triple1) -> (rule1 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
The cat is cold.
("cat" "is" "cold" "+")
int2
((((triple1) -> (rule4 % int2)) triple1) -> (rule1 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
The cat is cold.
("cat" "is" "cold" "+")
int2
The cat is red.
("cat" "is" "red" "+")
((((triple1) -> (rule5 % int2))) -> (rule8 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat is young.
("cat" "is" "young" "+")
int2
((((((triple1) -> (rule2 % int3)) triple1) -> (rule1 % int2))) -> (rule8 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat is young.
("cat" "is" "young" "+")
int2
The cat is cold.
("cat" "is" "cold" "+")
int3
((((((triple1) -> (rule4 % int3)) triple1) -> (rule1 % int2))) -> (rule8 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat is young.
("cat" "is" "young" "+")
int2
The cat is cold.
("cat" "is" "cold" "+")
int3
The cat is big.
("cat" "is" "big" "+")
((triple1 ((((triple1) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule3 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2
The cat is young.
("cat" "is" "young" "+")
int3
((triple1 ((((((triple1) -> (rule2 % int4)) triple1) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule3 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2
The cat is young.
("cat" "is" "young" "+")
int3
The cat is cold.
("cat" "is" "cold" "+")
int4
((triple1 ((((((triple1) -> (rule4 % int4)) triple1) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule3 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2
The cat is young.
("cat" "is" "young" "+")
int3
The cat is cold.
("cat" "is" "cold" "+")
int4