Charlie is big. Charlie is furry. Charlie is green. Charlie is nice. Dave is not big. Dave is green. Dave is white. Harry is green. Harry is not nice. Harry is not white. All big, nice things are not white. If something is kind and big then it is white. If something is quiet and big then it is not white.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Dave is not big.
("Dave" "is" "big" "-")
Dave is green.
("Dave" "is" "green" "+")
Dave is white.
("Dave" "is" "white" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is not nice.
("Harry" "is" "nice" "-")
Harry is not white.
("Harry" "is" "white" "-")
All big, nice things are not white.
((("something" "is" "big" "+") ("something" "is" "nice" "+")) -> ("something" "is" "white" "-"))
If something is kind and big then it is white.
((("something" "is" "kind" "+") ("something" "is" "big" "+")) -> ("something" "is" "white" "+"))
If something is quiet and big then it is not white.
((("something" "is" "quiet" "+") ("something" "is" "big" "+")) -> ("something" "is" "white" "-"))
Dave is white.
True
1
proof
[(triple7)]
("Dave" "is" "white" "+")
triple7
Charlie is not furry.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "furry" "-")
triple2
Charlie is not white.
True
3
proof
[(((triple1 triple4) -> rule1))]
("Charlie" "is" "white" "-")
((triple1 triple4) -> (rule1 % int1))
Charlie is not white.
("Charlie" "is" "white" "-")
int1
Charlie is white.
False
3
inv-proof
[(((triple1 triple4) -> rule1))]
("Charlie" "is" "white" "+")
((triple1 triple4) -> (rule1 % int1))
Charlie is not white.
("Charlie" "is" "white" "-")
int1
Charlie is not quiet.
Unknown
inv-random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "-")
Dave is nice.
Unknown
random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "+")
Harry is not quiet.
Unknown
inv-random
[@0: Harry is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "quiet" "-")
Harry is big.
Unknown
random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "+")
@0: Charlie is big.[(triple1)] Charlie is furry.[(triple2)] Charlie is green.[(triple3)] Charlie is nice.[(triple4)] Dave is green.[(triple6)] Dave is not big.[(triple5)] Dave is white.[(triple7)] Harry is green.[(triple8)] Harry is not nice.[(triple9)] Harry is not white.[(triple10)] @1: Charlie is not white.[(((triple1 triple4) -> rule1))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Charlie is furry.
("Charlie" "is" "furry" "+")
triple2
Charlie is green.
("Charlie" "is" "green" "+")
triple3
Charlie is nice.
("Charlie" "is" "nice" "+")
triple4
Dave is green.
("Dave" "is" "green" "+")
triple6
Dave is not big.
("Dave" "is" "big" "-")
triple5
Dave is white.
("Dave" "is" "white" "+")
triple7
Harry is green.
("Harry" "is" "green" "+")
triple8
Harry is not nice.
("Harry" "is" "nice" "-")
triple9
Harry is not white.
("Harry" "is" "white" "-")
triple10
Charlie is not white.
("Charlie" "is" "white" "-")
((triple1 triple4) -> (rule1 % int1))
Charlie is not white.
("Charlie" "is" "white" "-")
int1