Harry is not big. Harry is cold. Harry is green. If something is red and kind then it is not cold. Kind things are cold. If something is green then it is red. If something is nice and not kind then it is red. If Harry is green and Harry is not big then Harry is nice. All red, cold things are nice.
Harry is not big.
("Harry" "is" "big" "-")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is green.
("Harry" "is" "green" "+")
If something is red and kind then it is not cold.
((("something" "is" "red" "+") ("something" "is" "kind" "+")) -> ("something" "is" "cold" "-"))
Kind things are cold.
((("something" "is" "kind" "+")) -> ("something" "is" "cold" "+"))
If something is green then it is red.
((("something" "is" "green" "+")) -> ("something" "is" "red" "+"))
If something is nice and not kind then it is red.
((("something" "is" "nice" "+") ("something" "is" "kind" "~")) -> ("something" "is" "red" "+"))
If Harry is green and Harry is not big then Harry is nice.
((("Harry" "is" "green" "+") ("Harry" "is" "big" "~")) -> ("Harry" "is" "nice" "+"))
All red, cold things are nice.
((("something" "is" "red" "+") ("something" "is" "cold" "+")) -> ("something" "is" "nice" "+"))
Harry is not big.
True
1
proof
[(triple1)]
("Harry" "is" "big" "-")
triple1
Harry is not green.
False
1
inv-proof
[(triple3)]
("Harry" "is" "green" "-")
triple3
Harry is nice.
True
3
proof
[(((triple3 triple1) -> rule5) OR ((((triple3) -> rule3) triple2) -> rule6))]
("Harry" "is" "nice" "+")
((triple3 triple1) -> (rule5 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
((((triple3) -> (rule3 % int2)) triple2) -> (rule6 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is not red.
False
2
inv-proof
[(((triple3) -> rule3))]
("Harry" "is" "red" "-")
((triple3) -> (rule3 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is not quiet.
Unknown
inv-random
[@0: Harry is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "quiet" "-")
Harry is kind.
Unknown
random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "+")
@0: Harry is cold.[(triple2)] Harry is green.[(triple3)] Harry is not big.[(triple1)] @1: Harry is nice.[(((triple3 triple1) -> rule5) OR ((((triple3) -> rule3) triple2) -> rule6))] Harry is red.[(((triple3) -> rule3))]
Harry is cold.
("Harry" "is" "cold" "+")
triple2
Harry is green.
("Harry" "is" "green" "+")
triple3
Harry is not big.
("Harry" "is" "big" "-")
triple1
Harry is nice.
("Harry" "is" "nice" "+")
((triple3 triple1) -> (rule5 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
((((triple3) -> (rule3 % int2)) triple2) -> (rule6 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
((triple3) -> (rule3 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1