Anne is nice. Dave is big. Dave is furry. Dave is quiet. Dave is red. Fiona is nice. Fiona is red. Harry is big. Harry is furry. Harry is red. All quiet people are furry. If Dave is blue then Dave is quiet. Smart people are red. Blue, quiet people are big. All big, nice people are smart. If someone is nice then they are red. All furry, red people are quiet. If someone is blue then they are nice.
Anne is nice.
("Anne" "is" "nice" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is red.
("Dave" "is" "red" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is red.
("Harry" "is" "red" "+")
All quiet people are furry.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "furry" "+"))
If Dave is blue then Dave is quiet.
((("Dave" "is" "blue" "+")) -> ("Dave" "is" "quiet" "+"))
Smart people are red.
((("someone" "is" "smart" "+")) -> ("someone" "is" "red" "+"))
Blue, quiet people are big.
((("someone" "is" "blue" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "big" "+"))
All big, nice people are smart.
((("someone" "is" "big" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "smart" "+"))
If someone is nice then they are red.
((("someone" "is" "nice" "+")) -> ("someone" "is" "red" "+"))
All furry, red people are quiet.
((("someone" "is" "furry" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "quiet" "+"))
If someone is blue then they are nice.
((("someone" "is" "blue" "+")) -> ("someone" "is" "nice" "+"))
Dave is quiet.
True
1
proof
[(triple4 OR ((triple3 triple5) -> rule7))]
("Dave" "is" "quiet" "+")
triple4
((triple3 triple5) -> (rule7 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Anne is not nice.
False
1
inv-proof
[(triple1)]
("Anne" "is" "nice" "-")
triple1
Harry is quiet.
True
3
proof
[(((triple9 triple10) -> rule7))]
("Harry" "is" "quiet" "+")
((triple9 triple10) -> (rule7 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is not quiet.
False
3
inv-proof
[(((triple9 triple10) -> rule7))]
("Harry" "is" "quiet" "-")
((triple9 triple10) -> (rule7 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Anne is not furry.
Unknown
inv-rconc
[@2: Anne is furry.[CWA. Example of deepest failure = (rule1 <- rule7 <- FAIL)]]
("Anne" "is" "furry" "-")
Anne is smart.
Unknown
rconc
[@2: Anne is smart.[CWA. Example of deepest failure = (rule5 <- rule4 <- FAIL)]]
("Anne" "is" "smart" "+")
Harry is not blue.
Unknown
inv-random
[@0: Harry is blue.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "blue" "-")
Dave is blue.
Unknown
random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "+")
@0: Anne is nice.[(triple1)] Dave is big.[(triple2)] Dave is furry.[(triple3 OR ((triple4) -> rule1))] Dave is quiet.[(triple4 OR ((triple3 triple5) -> rule7))] Dave is red.[(triple5)] Fiona is nice.[(triple6)] Fiona is red.[(triple7 OR ((triple6) -> rule6))] Harry is big.[(triple8)] Harry is furry.[(triple9)] Harry is red.[(triple10)] @1: Anne is red.[(((triple1) -> rule6))] Harry is quiet.[(((triple9 triple10) -> rule7))]
Anne is nice.
("Anne" "is" "nice" "+")
triple1
Dave is big.
("Dave" "is" "big" "+")
triple2
Dave is furry.
("Dave" "is" "furry" "+")
triple3
((triple4) -> (rule1 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
triple4
((triple3 triple5) -> (rule7 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
triple5
Fiona is nice.
("Fiona" "is" "nice" "+")
triple6
Fiona is red.
("Fiona" "is" "red" "+")
triple7
((triple6) -> (rule6 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
triple8
Harry is furry.
("Harry" "is" "furry" "+")
triple9
Harry is red.
("Harry" "is" "red" "+")
triple10
Anne is red.
("Anne" "is" "red" "+")
((triple1) -> (rule6 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple9 triple10) -> (rule7 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1