Anne is not big. Bob is big. Harry is big. Harry is green. Harry is nice. Harry is not smart. Harry is white. All nice, smart people are not red. If someone is red and white then they are furry. All big, red people are not furry. If someone is white and not smart then they are not furry. All furry, white people are big. Furry people are nice.
Anne is not big.
("Anne" "is" "big" "-")
Bob is big.
("Bob" "is" "big" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is not smart.
("Harry" "is" "smart" "-")
Harry is white.
("Harry" "is" "white" "+")
All nice, smart people are not red.
((("someone" "is" "nice" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "red" "-"))
If someone is red and white then they are furry.
((("someone" "is" "red" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "furry" "+"))
All big, red people are not furry.
((("someone" "is" "big" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "furry" "-"))
If someone is white and not smart then they are not furry.
((("someone" "is" "white" "+") ("someone" "is" "smart" "~")) -> ("someone" "is" "furry" "-"))
All furry, white people are big.
((("someone" "is" "furry" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "big" "+"))
Furry people are nice.
((("someone" "is" "furry" "+")) -> ("someone" "is" "nice" "+"))
Bob is big.
True
1
proof
[(triple2)]
("Bob" "is" "big" "+")
triple2
Harry is not green.
False
1
inv-proof
[(triple4)]
("Harry" "is" "green" "-")
triple4
Harry is not furry.
True
3
proof
[(((triple7 triple6) -> rule4))]
("Harry" "is" "furry" "-")
((triple7 triple6) -> (rule4 % int1))
Harry is not furry.
("Harry" "is" "furry" "-")
int1
Harry is furry.
False
3
inv-proof
[(((triple7 triple6) -> rule4))]
("Harry" "is" "furry" "+")
((triple7 triple6) -> (rule4 % int1))
Harry is not furry.
("Harry" "is" "furry" "-")
int1
Bob is not furry.
Unknown
inv-rconc
[@1: Bob is furry.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "furry" "-")
Anne is furry.
Unknown
rconc
[@1: Anne is furry.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "furry" "+")
Anne is not green.
Unknown
inv-random
[@0: Anne is green.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "green" "-")
Bob is smart.
Unknown
random
[@0: Bob is smart.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "smart" "+")
@0: Anne is not big.[(triple1)] Bob is big.[(triple2)] Harry is big.[(triple3)] Harry is green.[(triple4)] Harry is nice.[(triple5)] Harry is not smart.[(triple6)] Harry is white.[(triple7)] @1: Harry is not furry.[(((triple7 triple6) -> rule4))]
Anne is not big.
("Anne" "is" "big" "-")
triple1
Bob is big.
("Bob" "is" "big" "+")
triple2
Harry is big.
("Harry" "is" "big" "+")
triple3
Harry is green.
("Harry" "is" "green" "+")
triple4
Harry is nice.
("Harry" "is" "nice" "+")
triple5
Harry is not smart.
("Harry" "is" "smart" "-")
triple6
Harry is white.
("Harry" "is" "white" "+")
triple7
Harry is not furry.
("Harry" "is" "furry" "-")
((triple7 triple6) -> (rule4 % int1))
Harry is not furry.
("Harry" "is" "furry" "-")
int1