Anne is quiet. Anne is young. Dave is furry. Dave is red. Dave is round. Dave is young. Harry is red. Harry is rough. Harry is round. Harry is young. Young people are round. If someone is furry and rough then they are quiet. If someone is quiet then they are red.
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is young.
("Anne" "is" "young" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is young.
("Dave" "is" "young" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is young.
("Harry" "is" "young" "+")
Young people are round.
((("someone" "is" "young" "+")) -> ("someone" "is" "round" "+"))
If someone is furry and rough then they are quiet.
((("someone" "is" "furry" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "quiet" "+"))
If someone is quiet then they are red.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "red" "+"))
Anne is quiet.
True
1
proof
[(triple1)]
("Anne" "is" "quiet" "+")
triple1
Anne is not young.
False
1
inv-proof
[(triple2)]
("Anne" "is" "young" "-")
triple2
Harry is not quiet.
Unknown
inv-rconc
[@1: Harry is quiet.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Harry" "is" "quiet" "-")
Anne is kind.
Unknown
random
[@0: Anne is kind.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "kind" "+")
@0: Anne is quiet.[(triple1)] Anne is young.[(triple2)] Dave is furry.[(triple3)] Dave is red.[(triple4)] Dave is round.[(triple5 OR ((triple6) -> rule1))] Dave is young.[(triple6)] Harry is red.[(triple7)] Harry is rough.[(triple8)] Harry is round.[(triple9 OR ((triple10) -> rule1))] Harry is young.[(triple10)] @1: Anne is red.[(((triple1) -> rule3))] Anne is round.[(((triple2) -> rule1))]
Anne is quiet.
("Anne" "is" "quiet" "+")
triple1
Anne is young.
("Anne" "is" "young" "+")
triple2
Dave is furry.
("Dave" "is" "furry" "+")
triple3
Dave is red.
("Dave" "is" "red" "+")
triple4
Dave is round.
("Dave" "is" "round" "+")
triple5
((triple6) -> (rule1 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
triple6
Harry is red.
("Harry" "is" "red" "+")
triple7
Harry is rough.
("Harry" "is" "rough" "+")
triple8
Harry is round.
("Harry" "is" "round" "+")
triple9
((triple10) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
triple10
Anne is red.
("Anne" "is" "red" "+")
((triple1) -> (rule3 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
((triple2) -> (rule1 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1