The cat is blue. If someone is blue then they are nice. If someone is nice then they are cold. Cold people are rough.
The cat is blue.
("cat" "is" "blue" "+")
If someone is blue then they are nice.
((("someone" "is" "blue" "+")) -> ("someone" "is" "nice" "+"))
If someone is nice then they are cold.
((("someone" "is" "nice" "+")) -> ("someone" "is" "cold" "+"))
Cold people are rough.
((("someone" "is" "cold" "+")) -> ("someone" "is" "rough" "+"))
The cat is blue.
True
1
proof
[(triple1)]
("cat" "is" "blue" "+")
triple1
The cat is not blue.
False
1
inv-proof
[(triple1)]
("cat" "is" "blue" "-")
triple1
The cat is nice.
True
2
proof
[(((triple1) -> rule1))]
("cat" "is" "nice" "+")
((triple1) -> (rule1 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cat is not nice.
False
2
inv-proof
[(((triple1) -> rule1))]
("cat" "is" "nice" "-")
((triple1) -> (rule1 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cat is cold.
True
3
proof
[(((((triple1) -> rule1)) -> rule2))]
("cat" "is" "cold" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
The cat is nice.
("cat" "is" "nice" "+")
int2
The cat is not cold.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule2))]
("cat" "is" "cold" "-")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
The cat is nice.
("cat" "is" "nice" "+")
int2
The cat is rough.
True
4
proof
[(((((((triple1) -> rule1)) -> rule2)) -> rule3))]
("cat" "is" "rough" "+")
((((((triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The cat is cold.
("cat" "is" "cold" "+")
int2
The cat is nice.
("cat" "is" "nice" "+")
int3
The cat is not rough.
False
4
inv-proof
[(((((((triple1) -> rule1)) -> rule2)) -> rule3))]
("cat" "is" "rough" "-")
((((((triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The cat is cold.
("cat" "is" "cold" "+")
int2
The cat is nice.
("cat" "is" "nice" "+")
int3
The cat is not big.
Unknown
inv-random
[@0: The cat is big.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "big" "-")
The cat eats the cat.
Unknown
random
[@0: The cat eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "cat" "+")
The cat does not chase the cat.
Unknown
inv-random
[@0: The cat chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "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 blue.[(triple1)] @1: The cat is nice.[(((triple1) -> rule1))] @2: The cat is cold.[(((((triple1) -> rule1)) -> rule2))] @3: The cat is rough.[(((((((triple1) -> rule1)) -> rule2)) -> rule3))]
The cat is blue.
("cat" "is" "blue" "+")
triple1
The cat is nice.
("cat" "is" "nice" "+")
((triple1) -> (rule1 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cat is cold.
("cat" "is" "cold" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
The cat is nice.
("cat" "is" "nice" "+")
int2
The cat is rough.
("cat" "is" "rough" "+")
((((((triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The cat is cold.
("cat" "is" "cold" "+")
int2
The cat is nice.
("cat" "is" "nice" "+")
int3