Charlie is big. Charlie is green. Charlie is smart. Harry is green. Harry is kind. Harry is nice. Harry is smart. If something is big and not red then it is not kind. All smart things are kind. Green, big things are nice.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is smart.
("Harry" "is" "smart" "+")
If something is big and not red then it is not kind.
((("something" "is" "big" "+") ("something" "is" "red" "~")) -> ("something" "is" "kind" "-"))
All smart things are kind.
((("something" "is" "smart" "+")) -> ("something" "is" "kind" "+"))
Green, big things are nice.
((("something" "is" "green" "+") ("something" "is" "big" "+")) -> ("something" "is" "nice" "+"))
Harry is nice.
True
1
proof
[(triple6)]
("Harry" "is" "nice" "+")
triple6
Harry is not nice.
False
1
inv-proof
[(triple6)]
("Harry" "is" "nice" "-")
triple6
Charlie is kind.
True
2
proof
[(((triple3) -> rule2))]
("Charlie" "is" "kind" "+")
((triple3) -> (rule2 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is not kind.
False
2
inv-proof
[(((triple3) -> rule2))]
("Charlie" "is" "kind" "-")
((triple3) -> (rule2 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Harry is not big.
Unknown
inv-random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "-")
Harry is red.
Unknown
random
[@0: Harry is red.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "red" "+")
Harry is not cold.
Unknown
inv-random
[@0: Harry is cold.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "cold" "-")
Charlie is red.
Unknown
random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "+")
@0: Charlie is big.[(triple1)] Charlie is green.[(triple2)] Charlie is smart.[(triple3)] Harry is green.[(triple4)] Harry is kind.[(triple5 OR ((triple7) -> rule2))] Harry is nice.[(triple6)] Harry is smart.[(triple7)] @1: Charlie is kind.[(((triple3) -> rule2))] Charlie is nice.[(((triple2 triple1) -> rule3))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Charlie is green.
("Charlie" "is" "green" "+")
triple2
Charlie is smart.
("Charlie" "is" "smart" "+")
triple3
Harry is green.
("Harry" "is" "green" "+")
triple4
Harry is kind.
("Harry" "is" "kind" "+")
triple5
((triple7) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
triple6
Harry is smart.
("Harry" "is" "smart" "+")
triple7
Charlie is kind.
("Charlie" "is" "kind" "+")
((triple3) -> (rule2 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
((triple2 triple1) -> (rule3 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1