Bob is not big. Bob is cold. Bob is furry. Bob is not young. Charlie is furry. Charlie is smart. Charlie is white. Charlie is young. Dave is big. Dave is not white. Harry is furry. Harry is green. If someone is young and not cold then they are not big. If someone is green then they are young. Furry, young people are green.
Bob is not big.
("Bob" "is" "big" "-")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is not young.
("Bob" "is" "young" "-")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is not white.
("Dave" "is" "white" "-")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is green.
("Harry" "is" "green" "+")
If someone is young and not cold then they are not big.
((("someone" "is" "young" "+") ("someone" "is" "cold" "~")) -> ("someone" "is" "big" "-"))
If someone is green then they are young.
((("someone" "is" "green" "+")) -> ("someone" "is" "young" "+"))
Furry, young people are green.
((("someone" "is" "furry" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "green" "+"))
Charlie is white.
True
1
proof
[(triple7)]
("Charlie" "is" "white" "+")
triple7
Harry is not furry.
False
1
inv-proof
[(triple11)]
("Harry" "is" "furry" "-")
triple11
Bob is not green.
Unknown
inv-rconc
[@1: Bob is green.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "green" "-")
Dave is cold.
Unknown
random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "+")
@0: Bob is cold.[(triple2)] Bob is furry.[(triple3)] Bob is not big.[(triple1)] Bob is not young.[(triple4)] Charlie is furry.[(triple5)] Charlie is smart.[(triple6)] Charlie is white.[(triple7)] Charlie is young.[(triple8)] Dave is big.[(triple9)] Dave is not white.[(triple10)] Harry is furry.[(triple11)] Harry is green.[(triple12)] @1: Charlie is green.[(((triple5 triple8) -> rule3))] Harry is young.[(((triple12) -> rule2))]
Bob is cold.
("Bob" "is" "cold" "+")
triple2
Bob is furry.
("Bob" "is" "furry" "+")
triple3
Bob is not big.
("Bob" "is" "big" "-")
triple1
Bob is not young.
("Bob" "is" "young" "-")
triple4
Charlie is furry.
("Charlie" "is" "furry" "+")
triple5
Charlie is smart.
("Charlie" "is" "smart" "+")
triple6
Charlie is white.
("Charlie" "is" "white" "+")
triple7
Charlie is young.
("Charlie" "is" "young" "+")
triple8
Dave is big.
("Dave" "is" "big" "+")
triple9
Dave is not white.
("Dave" "is" "white" "-")
triple10
Harry is furry.
("Harry" "is" "furry" "+")
triple11
Harry is green.
("Harry" "is" "green" "+")
triple12
Charlie is green.
("Charlie" "is" "green" "+")
((triple5 triple8) -> (rule3 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
((triple12) -> (rule2 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1