Anne is nice. Bob is nice. Harry is green. All big people are not white. If Harry is white and Harry is smart then Harry is rough. Green, big people are smart. All green people are big. If someone is big and nice then they are quiet. If someone is green and not rough then they are quiet.
Anne is nice.
("Anne" "is" "nice" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Harry is green.
("Harry" "is" "green" "+")
All big people are not white.
((("someone" "is" "big" "+")) -> ("someone" "is" "white" "-"))
If Harry is white and Harry is smart then Harry is rough.
((("Harry" "is" "white" "+") ("Harry" "is" "smart" "+")) -> ("Harry" "is" "rough" "+"))
Green, big people are smart.
((("someone" "is" "green" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "smart" "+"))
All green people are big.
((("someone" "is" "green" "+")) -> ("someone" "is" "big" "+"))
If someone is big and nice then they are quiet.
((("someone" "is" "big" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "quiet" "+"))
If someone is green and not rough then they are quiet.
((("someone" "is" "green" "+") ("someone" "is" "rough" "~")) -> ("someone" "is" "quiet" "+"))
Anne is nice.
True
1
proof
[(triple1)]
("Anne" "is" "nice" "+")
triple1
Bob is not nice.
False
1
inv-proof
[(triple2)]
("Bob" "is" "nice" "-")
triple2
Anne is not smart.
Unknown
inv-rconc
[@1: Anne is smart.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Anne" "is" "smart" "-")
Bob is green.
Unknown
random
[@0: Bob is green.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "green" "+")
@0: Anne is nice.[(triple1)] Bob is nice.[(triple2)] Harry is green.[(triple3)] @1: Harry is big.[(((triple3) -> rule4))] @2: Harry is not white.[(((((triple3) -> rule4)) -> rule1))] Harry is smart.[(((triple3 ((triple3) -> rule4)) -> rule3))]
Anne is nice.
("Anne" "is" "nice" "+")
triple1
Bob is nice.
("Bob" "is" "nice" "+")
triple2
Harry is green.
("Harry" "is" "green" "+")
triple3
Harry is big.
("Harry" "is" "big" "+")
((triple3) -> (rule4 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is not white.
("Harry" "is" "white" "-")
((((triple3) -> (rule4 % int2))) -> (rule1 % int1))
Harry is not white.
("Harry" "is" "white" "-")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
((triple3 ((triple3) -> (rule4 % int2))) -> (rule3 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2