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