Anne is not big. Anne is cold. Anne is kind. Charlie is cold. Charlie is kind. Charlie is nice. Charlie is quiet. Charlie is red. Harry is furry. Harry is nice. If something is kind then it is nice. If something is nice and not kind then it is not quiet.
Anne is not big.
("Anne" "is" "big" "-")
Anne is cold.
("Anne" "is" "cold" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is nice.
("Harry" "is" "nice" "+")
If something is kind then it is nice.
((("something" "is" "kind" "+")) -> ("something" "is" "nice" "+"))
If something is nice and not kind then it is not quiet.
((("something" "is" "nice" "+") ("something" "is" "kind" "~")) -> ("something" "is" "quiet" "-"))
Charlie is kind.
True
1
proof
[(triple5)]
("Charlie" "is" "kind" "+")
triple5
Anne is big.
False
1
inv-proof
[(triple1)]
("Anne" "is" "big" "+")
triple1
Anne is nice.
True
2
proof
[(((triple3) -> rule1))]
("Anne" "is" "nice" "+")
((triple3) -> (rule1 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is not nice.
False
2
inv-proof
[(((triple3) -> rule1))]
("Anne" "is" "nice" "-")
((triple3) -> (rule1 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Harry is not kind.
Unknown
inv-random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "-")
Anne is red.
Unknown
random
[@0: Anne is red.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "red" "+")
Harry is not quiet.
Unknown
inv-random
[@0: Harry is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "quiet" "-")
Charlie is big.
Unknown
random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "+")
@0: Anne is cold.[(triple2)] Anne is kind.[(triple3)] Anne is not big.[(triple1)] Charlie is cold.[(triple4)] Charlie is kind.[(triple5)] Charlie is nice.[(triple6 OR ((triple5) -> rule1))] Charlie is quiet.[(triple7)] Charlie is red.[(triple8)] Harry is furry.[(triple9)] Harry is nice.[(triple10)] @1: Anne is nice.[(((triple3) -> rule1))]
Anne is cold.
("Anne" "is" "cold" "+")
triple2
Anne is kind.
("Anne" "is" "kind" "+")
triple3
Anne is not big.
("Anne" "is" "big" "-")
triple1
Charlie is cold.
("Charlie" "is" "cold" "+")
triple4
Charlie is kind.
("Charlie" "is" "kind" "+")
triple5
Charlie is nice.
("Charlie" "is" "nice" "+")
triple6
((triple5) -> (rule1 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple7
Charlie is red.
("Charlie" "is" "red" "+")
triple8
Harry is furry.
("Harry" "is" "furry" "+")
triple9
Harry is nice.
("Harry" "is" "nice" "+")
triple10
Anne is nice.
("Anne" "is" "nice" "+")
((triple3) -> (rule1 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1