Charlie is red. Charlie is not round. Dave is red. Dave is round. Harry is not big. Harry is white. Harry is not young. If something is white and not young then it is round.
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is not round.
("Charlie" "is" "round" "-")
Dave is red.
("Dave" "is" "red" "+")
Dave is round.
("Dave" "is" "round" "+")
Harry is not big.
("Harry" "is" "big" "-")
Harry is white.
("Harry" "is" "white" "+")
Harry is not young.
("Harry" "is" "young" "-")
If something is white and not young then it is round.
((("something" "is" "white" "+") ("something" "is" "young" "~")) -> ("something" "is" "round" "+"))
Charlie is red.
True
1
proof
[(triple1)]
("Charlie" "is" "red" "+")
triple1
Harry is big.
False
1
inv-proof
[(triple5)]
("Harry" "is" "big" "+")
triple5
Harry is round.
True
3
proof
[(((triple6 triple7) -> rule1))]
("Harry" "is" "round" "+")
((triple6 triple7) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is not round.
False
3
inv-proof
[(((triple6 triple7) -> rule1))]
("Harry" "is" "round" "-")
((triple6 triple7) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Charlie is not smart.
Unknown
inv-random
[@0: Charlie is smart.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "smart" "-")
Dave is white.
Unknown
random
[@0: Dave is white.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "white" "+")
Charlie is not furry.
Unknown
inv-random
[@0: Charlie is furry.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "furry" "-")
Dave is big.
Unknown
random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "+")
@0: Charlie is not round.[(triple2)] Charlie is red.[(triple1)] Dave is red.[(triple3)] Dave is round.[(triple4)] Harry is not big.[(triple5)] Harry is not young.[(triple7)] Harry is white.[(triple6)] @1: Harry is round.[(((triple6 triple7) -> rule1))]
Charlie is not round.
("Charlie" "is" "round" "-")
triple2
Charlie is red.
("Charlie" "is" "red" "+")
triple1
Dave is red.
("Dave" "is" "red" "+")
triple3
Dave is round.
("Dave" "is" "round" "+")
triple4
Harry is not big.
("Harry" "is" "big" "-")
triple5
Harry is not young.
("Harry" "is" "young" "-")
triple7
Harry is white.
("Harry" "is" "white" "+")
triple6
Harry is round.
("Harry" "is" "round" "+")
((triple6 triple7) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1