Bob is smart. Dave is smart. Fiona is green. Harry is white. White people are quiet. If someone is white and not round then they are not quiet. If someone is green and smart then they are not white.
Bob is smart.
("Bob" "is" "smart" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Harry is white.
("Harry" "is" "white" "+")
White people are quiet.
((("someone" "is" "white" "+")) -> ("someone" "is" "quiet" "+"))
If someone is white and not round then they are not quiet.
((("someone" "is" "white" "+") ("someone" "is" "round" "~")) -> ("someone" "is" "quiet" "-"))
If someone is green and smart then they are not white.
((("someone" "is" "green" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "white" "-"))
Dave is smart.
True
1
proof
[(triple2)]
("Dave" "is" "smart" "+")
triple2
Fiona is not green.
False
1
inv-proof
[(triple3)]
("Fiona" "is" "green" "-")
triple3
Harry is quiet.
True
2
proof
[(((triple4) -> rule1))]
("Harry" "is" "quiet" "+")
((triple4) -> (rule1 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is not quiet.
False
2
inv-proof
[(((triple4) -> rule1))]
("Harry" "is" "quiet" "-")
((triple4) -> (rule1 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Fiona is not quiet.
Unknown
inv-rconc
[@1: Fiona is quiet.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "quiet" "-")
Dave is quiet.
Unknown
rconc
[@1: Dave is quiet.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "quiet" "+")
Dave is not kind.
Unknown
inv-random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "-")
Harry is round.
Unknown
random
[@0: Harry is round.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "round" "+")
@0: Bob is smart.[(triple1)] Dave is smart.[(triple2)] Fiona is green.[(triple3)] Harry is white.[(triple4)] @1: Harry is quiet.[(((triple4) -> rule1))]
Bob is smart.
("Bob" "is" "smart" "+")
triple1
Dave is smart.
("Dave" "is" "smart" "+")
triple2
Fiona is green.
("Fiona" "is" "green" "+")
triple3
Harry is white.
("Harry" "is" "white" "+")
triple4
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple4) -> (rule1 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1