The cat is nice. Rough, nice things are cold. All nice things are cold. If the cat is kind and the cat is cold then the cat is not rough. If the cat is big then the cat is not rough. If something is rough and cold then it is not nice. Big, kind things are nice. Rough things are nice. Cold things are kind.
The cat is nice.
("cat" "is" "nice" "+")
Rough, nice things are cold.
((("something" "is" "rough" "+") ("something" "is" "nice" "+")) -> ("something" "is" "cold" "+"))
All nice things are cold.
((("something" "is" "nice" "+")) -> ("something" "is" "cold" "+"))
If the cat is kind and the cat is cold then the cat is not rough.
((("cat" "is" "kind" "+") ("cat" "is" "cold" "+")) -> ("cat" "is" "rough" "-"))
If the cat is big then the cat is not rough.
((("cat" "is" "big" "+")) -> ("cat" "is" "rough" "-"))
If something is rough and cold then it is not nice.
((("something" "is" "rough" "+") ("something" "is" "cold" "+")) -> ("something" "is" "nice" "-"))
Big, kind things are nice.
((("something" "is" "big" "+") ("something" "is" "kind" "+")) -> ("something" "is" "nice" "+"))
Rough things are nice.
((("something" "is" "rough" "+")) -> ("something" "is" "nice" "+"))
Cold things are kind.
((("something" "is" "cold" "+")) -> ("something" "is" "kind" "+"))
The cat is nice.
True
1
proof
[(triple1)]
("cat" "is" "nice" "+")
triple1
The cat is not nice.
False
1
inv-proof
[(triple1)]
("cat" "is" "nice" "-")
triple1
The cat is cold.
True
2
proof
[(((triple1) -> rule2))]
("cat" "is" "cold" "+")
((triple1) -> (rule2 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
The cat is not cold.
False
2
inv-proof
[(((triple1) -> rule2))]
("cat" "is" "cold" "-")
((triple1) -> (rule2 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
The cat is kind.
True
3
proof
[(((((triple1) -> rule2)) -> rule8))]
("cat" "is" "kind" "+")
((((triple1) -> (rule2 % int2))) -> (rule8 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The cat is cold.
("cat" "is" "cold" "+")
int2
The cat is not kind.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule8))]
("cat" "is" "kind" "-")
((((triple1) -> (rule2 % int2))) -> (rule8 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The cat is cold.
("cat" "is" "cold" "+")
int2
The cat is not rough.
True
6
proof
[(((((((triple1) -> rule2)) -> rule8) ((triple1) -> rule2)) -> rule3))]
("cat" "is" "rough" "-")
((((((triple1) -> (rule2 % int3))) -> (rule8 % int2)) ((triple1) -> (rule2 % int3))) -> (rule3 % int1))
The cat is not rough.
("cat" "is" "rough" "-")
int1
The cat is kind.
("cat" "is" "kind" "+")
int2
The cat is cold.
("cat" "is" "cold" "+")
int3
The cat is rough.
False
6
inv-proof
[(((((((triple1) -> rule2)) -> rule8) ((triple1) -> rule2)) -> rule3))]
("cat" "is" "rough" "+")
((((((triple1) -> (rule2 % int3))) -> (rule8 % int2)) ((triple1) -> (rule2 % int3))) -> (rule3 % int1))
The cat is not rough.
("cat" "is" "rough" "-")
int1
The cat is kind.
("cat" "is" "kind" "+")
int2
The cat is cold.
("cat" "is" "cold" "+")
int3
The cat does not see the cat.
Unknown
inv-random
[@0: The cat sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "cat" "-")
The cat likes the cat.
Unknown
random
[@0: The cat likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "cat" "+")
The cat is not big.
Unknown
inv-random
[@0: The cat is big.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "big" "-")
The cat needs the cat.
Unknown
random
[@0: The cat needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "cat" "+")
@0: The cat is nice.[(triple1)] @1: The cat is cold.[(((triple1) -> rule2))] @2: The cat is kind.[(((((triple1) -> rule2)) -> rule8))] @3: The cat is not rough.[(((((((triple1) -> rule2)) -> rule8) ((triple1) -> rule2)) -> rule3))]
The cat is nice.
("cat" "is" "nice" "+")
triple1
The cat is cold.
("cat" "is" "cold" "+")
((triple1) -> (rule2 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
The cat is kind.
("cat" "is" "kind" "+")
((((triple1) -> (rule2 % int2))) -> (rule8 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The cat is cold.
("cat" "is" "cold" "+")
int2
The cat is not rough.
("cat" "is" "rough" "-")
((((((triple1) -> (rule2 % int3))) -> (rule8 % int2)) ((triple1) -> (rule2 % int3))) -> (rule3 % int1))
The cat is not rough.
("cat" "is" "rough" "-")
int1
The cat is kind.
("cat" "is" "kind" "+")
int2
The cat is cold.
("cat" "is" "cold" "+")
int3