Charlie is big. Charlie is not nice. Charlie is quiet. Charlie is not white. Dave is big. Dave is blue. Dave is nice. Gary is nice. Harry is big. Harry is nice. Harry is quiet. Harry is red. If something is red then it is blue. If something is white and big then it is quiet.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is not nice.
("Charlie" "is" "nice" "-")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is not white.
("Charlie" "is" "white" "-")
Dave is big.
("Dave" "is" "big" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is red.
("Harry" "is" "red" "+")
If something is red then it is blue.
((("something" "is" "red" "+")) -> ("something" "is" "blue" "+"))
If something is white and big then it is quiet.
((("something" "is" "white" "+") ("something" "is" "big" "+")) -> ("something" "is" "quiet" "+"))
Harry is big.
True
1
proof
[(triple9)]
("Harry" "is" "big" "+")
triple9
Harry is not nice.
False
1
inv-proof
[(triple10)]
("Harry" "is" "nice" "-")
triple10
Charlie is not blue.
Unknown
inv-rconc
[@1: Charlie is blue.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "blue" "-")
Harry is round.
Unknown
random
[@0: Harry is round.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "round" "+")
@0: Charlie is big.[(triple1)] Charlie is not nice.[(triple2)] Charlie is not white.[(triple4)] Charlie is quiet.[(triple3)] Dave is big.[(triple5)] Dave is blue.[(triple6)] Dave is nice.[(triple7)] Gary is nice.[(triple8)] Harry is big.[(triple9)] Harry is nice.[(triple10)] Harry is quiet.[(triple11)] Harry is red.[(triple12)] @1: Harry is blue.[(((triple12) -> rule1))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Charlie is not nice.
("Charlie" "is" "nice" "-")
triple2
Charlie is not white.
("Charlie" "is" "white" "-")
triple4
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple3
Dave is big.
("Dave" "is" "big" "+")
triple5
Dave is blue.
("Dave" "is" "blue" "+")
triple6
Dave is nice.
("Dave" "is" "nice" "+")
triple7
Gary is nice.
("Gary" "is" "nice" "+")
triple8
Harry is big.
("Harry" "is" "big" "+")
triple9
Harry is nice.
("Harry" "is" "nice" "+")
triple10
Harry is quiet.
("Harry" "is" "quiet" "+")
triple11
Harry is red.
("Harry" "is" "red" "+")
triple12
Harry is blue.
("Harry" "is" "blue" "+")
((triple12) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1