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