Anne is round. Charlie is quiet. Dave is not white. Harry is kind. If something is quiet and round then it is young. If something is kind and smart then it is not round. If something is kind and not quiet then it is smart. All round things are smart. If Charlie is quiet then Charlie is white. If Harry is not round then Harry is young. If something is quiet and not young then it is white. All young things are white.
Anne is round.
("Anne" "is" "round" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Dave is not white.
("Dave" "is" "white" "-")
Harry is kind.
("Harry" "is" "kind" "+")
If something is quiet and round then it is young.
((("something" "is" "quiet" "+") ("something" "is" "round" "+")) -> ("something" "is" "young" "+"))
If something is kind and smart then it is not round.
((("something" "is" "kind" "+") ("something" "is" "smart" "+")) -> ("something" "is" "round" "-"))
If something is kind and not quiet then it is smart.
((("something" "is" "kind" "+") ("something" "is" "quiet" "~")) -> ("something" "is" "smart" "+"))
All round things are smart.
((("something" "is" "round" "+")) -> ("something" "is" "smart" "+"))
If Charlie is quiet then Charlie is white.
((("Charlie" "is" "quiet" "+")) -> ("Charlie" "is" "white" "+"))
If Harry is not round then Harry is young.
((("Harry" "is" "round" "~")) -> ("Harry" "is" "young" "+"))
If something is quiet and not young then it is white.
((("something" "is" "quiet" "+") ("something" "is" "young" "~")) -> ("something" "is" "white" "+"))
All young things are white.
((("something" "is" "young" "+")) -> ("something" "is" "white" "+"))
Dave is not white.
True
1
proof
[(triple3)]
("Dave" "is" "white" "-")
triple3
Anne is not round.
False
1
inv-proof
[(triple1)]
("Anne" "is" "round" "-")
triple1
Anne is smart.
True
2
proof
[(((triple1) -> rule4))]
("Anne" "is" "smart" "+")
((triple1) -> (rule4 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is not smart.
False
2
inv-proof
[(((triple1) -> rule4))]
("Anne" "is" "smart" "-")
((triple1) -> (rule4 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is not young.
Unknown
inv-rconc
[@1: Anne is young.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "young" "-")
Charlie is smart.
Unknown
rconc
[@1: Charlie is smart.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "smart" "+")
Harry is not green.
Unknown
inv-random
[@0: Harry is green.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "green" "-")
Dave is round.
Unknown
random
[@0: Dave is round.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "round" "+")
@0: Anne is round.[(triple1)] Charlie is quiet.[(triple2)] Dave is not white.[(triple3)] Harry is kind.[(triple4)] @1: Anne is smart.[(((triple1) -> rule4))] Charlie is white.[(((triple2) -> rule5))]
Anne is round.
("Anne" "is" "round" "+")
triple1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple2
Dave is not white.
("Dave" "is" "white" "-")
triple3
Harry is kind.
("Harry" "is" "kind" "+")
triple4
Anne is smart.
("Anne" "is" "smart" "+")
((triple1) -> (rule4 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
((triple2) -> (rule5 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1