Bob is quiet. Bob is round. Charlie is not big. Fiona is not red. Harry is kind. Harry is not quiet. Harry is red. Kind people are not quiet. If someone is big and cold then they are not kind. If someone is kind and not big then they are red.
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is round.
("Bob" "is" "round" "+")
Charlie is not big.
("Charlie" "is" "big" "-")
Fiona is not red.
("Fiona" "is" "red" "-")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is not quiet.
("Harry" "is" "quiet" "-")
Harry is red.
("Harry" "is" "red" "+")
Kind people are not quiet.
((("someone" "is" "kind" "+")) -> ("someone" "is" "quiet" "-"))
If someone is big and cold then they are not kind.
((("someone" "is" "big" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "kind" "-"))
If someone is kind and not big then they are red.
((("someone" "is" "kind" "+") ("someone" "is" "big" "~")) -> ("someone" "is" "red" "+"))
Charlie is not big.
True
1
proof
[(triple3)]
("Charlie" "is" "big" "-")
triple3
Bob is not quiet.
False
1
inv-proof
[(triple1)]
("Bob" "is" "quiet" "-")
triple1
Bob is not red.
Unknown
inv-rconc
[@1: Bob is red.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "red" "-")
Bob is kind.
Unknown
random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "+")
@0: Bob is quiet.[(triple1)] Bob is round.[(triple2)] Charlie is not big.[(triple3)] Fiona is not red.[(triple4)] Harry is kind.[(triple5)] Harry is not quiet.[(triple6 OR ((triple5) -> rule1))] Harry is red.[(triple7)]
Bob is quiet.
("Bob" "is" "quiet" "+")
triple1
Bob is round.
("Bob" "is" "round" "+")
triple2
Charlie is not big.
("Charlie" "is" "big" "-")
triple3
Fiona is not red.
("Fiona" "is" "red" "-")
triple4
Harry is kind.
("Harry" "is" "kind" "+")
triple5
Harry is not quiet.
("Harry" "is" "quiet" "-")
triple6
((triple5) -> (rule1 % int1))
Harry is not quiet.
("Harry" "is" "quiet" "-")
int1
Harry is red.
("Harry" "is" "red" "+")
triple7