The cat is blue. If someone is big then they are cold. All big, blue people are not cold. Blue people are cold. If the cat is round then the cat is cold. If the cat is not big then the cat is not cold. If someone is cold and blue then they are not kind. If the cat is not round then the cat is not blue. If the cat is kind then the cat is blue.
The cat is blue.
("cat" "is" "blue" "+")
If someone is big then they are cold.
((("someone" "is" "big" "+")) -> ("someone" "is" "cold" "+"))
All big, blue people are not cold.
((("someone" "is" "big" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "cold" "-"))
Blue people are cold.
((("someone" "is" "blue" "+")) -> ("someone" "is" "cold" "+"))
If the cat is round then the cat is cold.
((("cat" "is" "round" "+")) -> ("cat" "is" "cold" "+"))
If the cat is not big then the cat is not cold.
((("cat" "is" "big" "~")) -> ("cat" "is" "cold" "-"))
If someone is cold and blue then they are not kind.
((("someone" "is" "cold" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "kind" "-"))
If the cat is not round then the cat is not blue.
((("cat" "is" "round" "~")) -> ("cat" "is" "blue" "-"))
If the cat is kind then the cat is blue.
((("cat" "is" "kind" "+")) -> ("cat" "is" "blue" "+"))
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 cold.
True
2
proof
[(((triple1) -> rule3))]
("cat" "is" "cold" "+")
((triple1) -> (rule3 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
The cat is not cold.
False
2
inv-proof
[(((triple1) -> rule3))]
("cat" "is" "cold" "-")
((triple1) -> (rule3 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
The cat is not kind.
True
4
proof
[(((((triple1) -> rule3) triple1) -> rule6))]
("cat" "is" "kind" "-")
((((triple1) -> (rule3 % int2)) triple1) -> (rule6 % int1))
The cat is not kind.
("cat" "is" "kind" "-")
int1
The cat is cold.
("cat" "is" "cold" "+")
int2
The cat is kind.
False
4
inv-proof
[(((((triple1) -> rule3) triple1) -> rule6))]
("cat" "is" "kind" "+")
((((triple1) -> (rule3 % int2)) triple1) -> (rule6 % int1))
The cat is not kind.
("cat" "is" "kind" "-")
int1
The cat is cold.
("cat" "is" "cold" "+")
int2
The cat is not round.
Unknown
inv-random
[@0: The cat is round.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "round" "-")
The cat eats the cat.
Unknown
random
[@0: The cat eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "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 sees the cat.
Unknown
random
[@0: The cat sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "cat" "+")
@0: The cat is blue.[(triple1)] @1: The cat is cold.[(((triple1) -> rule3))] @2: The cat is not kind.[(((((triple1) -> rule3) triple1) -> rule6))]
The cat is blue.
("cat" "is" "blue" "+")
triple1
The cat is cold.
("cat" "is" "cold" "+")
((triple1) -> (rule3 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
The cat is not kind.
("cat" "is" "kind" "-")
((((triple1) -> (rule3 % int2)) triple1) -> (rule6 % int1))
The cat is not kind.
("cat" "is" "kind" "-")
int1
The cat is cold.
("cat" "is" "cold" "+")
int2