Anne is big. Anne is blue. Anne is cold. Anne is furry. Anne is not quiet. Anne is round. Anne is not smart. Dave is not furry. Dave is quiet. Harry is not big. Harry is blue. Harry is furry. Harry is quiet. Harry is round. Harry is not smart. If Anne is furry then Anne is blue. If someone is blue then they are round. If someone is blue then they are furry. If someone is smart then they are furry. If Harry is round then Harry is quiet. If Dave is big then Dave is not round. Quiet, smart people are big. If someone is round and not blue then they are not cold.
Anne is big.
("Anne" "is" "big" "+")
Anne is blue.
("Anne" "is" "blue" "+")
Anne is cold.
("Anne" "is" "cold" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is not quiet.
("Anne" "is" "quiet" "-")
Anne is round.
("Anne" "is" "round" "+")
Anne is not smart.
("Anne" "is" "smart" "-")
Dave is not furry.
("Dave" "is" "furry" "-")
Dave is quiet.
("Dave" "is" "quiet" "+")
Harry is not big.
("Harry" "is" "big" "-")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is not smart.
("Harry" "is" "smart" "-")
If Anne is furry then Anne is blue.
((("Anne" "is" "furry" "+")) -> ("Anne" "is" "blue" "+"))
If someone is blue then they are round.
((("someone" "is" "blue" "+")) -> ("someone" "is" "round" "+"))
If someone is blue then they are furry.
((("someone" "is" "blue" "+")) -> ("someone" "is" "furry" "+"))
If someone is smart then they are furry.
((("someone" "is" "smart" "+")) -> ("someone" "is" "furry" "+"))
If Harry is round then Harry is quiet.
((("Harry" "is" "round" "+")) -> ("Harry" "is" "quiet" "+"))
If Dave is big then Dave is not round.
((("Dave" "is" "big" "+")) -> ("Dave" "is" "round" "-"))
Quiet, smart people are big.
((("someone" "is" "quiet" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "big" "+"))
If someone is round and not blue then they are not cold.
((("someone" "is" "round" "+") ("someone" "is" "blue" "~")) -> ("someone" "is" "cold" "-"))
Dave is quiet.
True
1
proof
[(triple9)]
("Dave" "is" "quiet" "+")
triple9
Dave is not quiet.
False
1
inv-proof
[(triple9)]
("Dave" "is" "quiet" "-")
triple9
Dave is not big.
Unknown
inv-rconc
[@1: Dave is big.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Dave" "is" "big" "-")
Dave is cold.
Unknown
random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "+")
@0: Anne is big.[(triple1)] Anne is blue.[(triple2 OR ((triple4) -> rule1))] Anne is cold.[(triple3)] Anne is furry.[(triple4 OR ((triple2) -> rule3))] Anne is not quiet.[(triple5)] Anne is not smart.[(triple7)] Anne is round.[(triple6 OR ((triple2) -> rule2) OR ((((triple4) -> rule1)) -> rule2))] Dave is not furry.[(triple8)] Dave is quiet.[(triple9)] Harry is blue.[(triple11)] Harry is furry.[(triple12 OR ((triple11) -> rule3))] Harry is not big.[(triple10)] Harry is not smart.[(triple15)] Harry is quiet.[(triple13 OR ((triple14) -> rule5) OR ((((triple11) -> rule2)) -> rule5))] Harry is round.[(triple14 OR ((triple11) -> rule2))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is blue.
("Anne" "is" "blue" "+")
triple2
((triple4) -> (rule1 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
triple3
Anne is furry.
("Anne" "is" "furry" "+")
triple4
((triple2) -> (rule3 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is not quiet.
("Anne" "is" "quiet" "-")
triple5
Anne is not smart.
("Anne" "is" "smart" "-")
triple7
Anne is round.
("Anne" "is" "round" "+")
triple6
((triple2) -> (rule2 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
((((triple4) -> (rule1 % int2))) -> (rule2 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Dave is not furry.
("Dave" "is" "furry" "-")
triple8
Dave is quiet.
("Dave" "is" "quiet" "+")
triple9
Harry is blue.
("Harry" "is" "blue" "+")
triple11
Harry is furry.
("Harry" "is" "furry" "+")
triple12
((triple11) -> (rule3 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is not big.
("Harry" "is" "big" "-")
triple10
Harry is not smart.
("Harry" "is" "smart" "-")
triple15
Harry is quiet.
("Harry" "is" "quiet" "+")
triple13
((triple14) -> (rule5 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
((((triple11) -> (rule2 % int2))) -> (rule5 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
triple14
((triple11) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1