Harry is big. All nice, quiet people are not blue. All nice, kind people are big. All quiet people are kind. If someone is big then they are quiet. All round, kind people are cold. If someone is blue and not quiet then they are round. If Harry is kind and Harry is not quiet then Harry is blue. If Harry is round and Harry is not quiet then Harry is blue.
Harry is big.
("Harry" "is" "big" "+")
All nice, quiet people are not blue.
((("someone" "is" "nice" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "blue" "-"))
All nice, kind people are big.
((("someone" "is" "nice" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "big" "+"))
All quiet people are kind.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "kind" "+"))
If someone is big then they are quiet.
((("someone" "is" "big" "+")) -> ("someone" "is" "quiet" "+"))
All round, kind people are cold.
((("someone" "is" "round" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "cold" "+"))
If someone is blue and not quiet then they are round.
((("someone" "is" "blue" "+") ("someone" "is" "quiet" "~")) -> ("someone" "is" "round" "+"))
If Harry is kind and Harry is not quiet then Harry is blue.
((("Harry" "is" "kind" "+") ("Harry" "is" "quiet" "~")) -> ("Harry" "is" "blue" "+"))
If Harry is round and Harry is not quiet then Harry is blue.
((("Harry" "is" "round" "+") ("Harry" "is" "quiet" "~")) -> ("Harry" "is" "blue" "+"))
Harry is big.
True
1
proof
[(triple1)]
("Harry" "is" "big" "+")
triple1
Harry is not big.
False
1
inv-proof
[(triple1)]
("Harry" "is" "big" "-")
triple1
Harry is quiet.
True
2
proof
[(((triple1) -> rule4))]
("Harry" "is" "quiet" "+")
((triple1) -> (rule4 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is not quiet.
False
2
inv-proof
[(((triple1) -> rule4))]
("Harry" "is" "quiet" "-")
((triple1) -> (rule4 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is kind.
True
3
proof
[(((((triple1) -> rule4)) -> rule3))]
("Harry" "is" "kind" "+")
((((triple1) -> (rule4 % int2))) -> (rule3 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is not kind.
False
3
inv-proof
[(((((triple1) -> rule4)) -> rule3))]
("Harry" "is" "kind" "-")
((((triple1) -> (rule4 % int2))) -> (rule3 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is not round.
Unknown
inv-rconc
[@1: Harry is round.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Harry" "is" "round" "-")
Harry is cold.
Unknown
rconc
[@2: Harry is cold.[CWA. Example of deepest failure = (rule5 <- rule6 <- FAIL)]]
("Harry" "is" "cold" "+")
Harry is not blue.
Unknown
inv-rconc
[@1: Harry is blue.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Harry" "is" "blue" "-")
Harry is nice.
Unknown
random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "+")
@0: Harry is big.[(triple1)] @1: Harry is quiet.[(((triple1) -> rule4))] @2: Harry is kind.[(((((triple1) -> rule4)) -> rule3))]
Harry is big.
("Harry" "is" "big" "+")
triple1
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple1) -> (rule4 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
((((triple1) -> (rule4 % int2))) -> (rule3 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2