The cat is cold. All round people are not nice. Rough, cold people are nice. If someone is rough and round then they are nice. If someone is rough and not cold then they are nice. If someone is round and not rough then they are nice. If the cat is rough and the cat is round then the cat is not nice. If the cat is nice then the cat is not big. If someone is cold then they are round.
The cat is cold.
("cat" "is" "cold" "+")
All round people are not nice.
((("someone" "is" "round" "+")) -> ("someone" "is" "nice" "-"))
Rough, cold people are nice.
((("someone" "is" "rough" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "nice" "+"))
If someone is rough and round then they are nice.
((("someone" "is" "rough" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "nice" "+"))
If someone is rough and not cold then they are nice.
((("someone" "is" "rough" "+") ("someone" "is" "cold" "~")) -> ("someone" "is" "nice" "+"))
If someone is round and not rough then they are nice.
((("someone" "is" "round" "+") ("someone" "is" "rough" "~")) -> ("someone" "is" "nice" "+"))
If the cat is rough and the cat is round then the cat is not nice.
((("cat" "is" "rough" "+") ("cat" "is" "round" "+")) -> ("cat" "is" "nice" "-"))
If the cat is nice then the cat is not big.
((("cat" "is" "nice" "+")) -> ("cat" "is" "big" "-"))
If someone is cold then they are round.
((("someone" "is" "cold" "+")) -> ("someone" "is" "round" "+"))
The cat is cold.
True
1
proof
[(triple1)]
("cat" "is" "cold" "+")
triple1
The cat is not cold.
False
1
inv-proof
[(triple1)]
("cat" "is" "cold" "-")
triple1
The cat is round.
True
2
proof
[(((triple1) -> rule8))]
("cat" "is" "round" "+")
((triple1) -> (rule8 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The cat is not round.
False
2
inv-proof
[(((triple1) -> rule8))]
("cat" "is" "round" "-")
((triple1) -> (rule8 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The cat is not nice.
True
3
proof
[(((((triple1) -> rule8)) -> rule1))]
("cat" "is" "nice" "-")
((((triple1) -> (rule8 % int2))) -> (rule1 % int1))
The cat is not nice.
("cat" "is" "nice" "-")
int1
The cat is round.
("cat" "is" "round" "+")
int2
The cat is nice.
False
3
inv-proof
[(((((triple1) -> rule8)) -> rule1))]
("cat" "is" "nice" "+")
((((triple1) -> (rule8 % int2))) -> (rule1 % int1))
The cat is not nice.
("cat" "is" "nice" "-")
int1
The cat is round.
("cat" "is" "round" "+")
int2
The cat does not like the cat.
Unknown
inv-random
[@0: The cat likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "cat" "-")
The cat is rough.
Unknown
random
[@0: The cat is rough.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "rough" "+")
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 visits the cat.
Unknown
random
[@0: The cat visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "cat" "+")
@0: The cat is cold.[(triple1)] @1: The cat is round.[(((triple1) -> rule8))] @2: The cat is not nice.[(((((triple1) -> rule8)) -> rule1))]
The cat is cold.
("cat" "is" "cold" "+")
triple1
The cat is round.
("cat" "is" "round" "+")
((triple1) -> (rule8 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The cat is not nice.
("cat" "is" "nice" "-")
((((triple1) -> (rule8 % int2))) -> (rule1 % int1))
The cat is not nice.
("cat" "is" "nice" "-")
int1
The cat is round.
("cat" "is" "round" "+")
int2