Charlie is nice. Gary is nice. Harry is kind. All kind people are not blue. If Harry is white then Harry is blue. If someone is kind and not blue then they are quiet. All quiet, kind people are smart. If someone is blue then they are not smart. If Gary is quiet then Gary is white.
Charlie is nice.
("Charlie" "is" "nice" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Harry is kind.
("Harry" "is" "kind" "+")
All kind people are not blue.
((("someone" "is" "kind" "+")) -> ("someone" "is" "blue" "-"))
If Harry is white then Harry is blue.
((("Harry" "is" "white" "+")) -> ("Harry" "is" "blue" "+"))
If someone is kind and not blue then they are quiet.
((("someone" "is" "kind" "+") ("someone" "is" "blue" "~")) -> ("someone" "is" "quiet" "+"))
All quiet, kind people are smart.
((("someone" "is" "quiet" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "smart" "+"))
If someone is blue then they are not smart.
((("someone" "is" "blue" "+")) -> ("someone" "is" "smart" "-"))
If Gary is quiet then Gary is white.
((("Gary" "is" "quiet" "+")) -> ("Gary" "is" "white" "+"))
Charlie is nice.
True
1
proof
[(triple1)]
("Charlie" "is" "nice" "+")
triple1
Gary is not nice.
False
1
inv-proof
[(triple2)]
("Gary" "is" "nice" "-")
triple2
Harry is not blue.
True
2
proof
[(((triple3) -> rule1))]
("Harry" "is" "blue" "-")
((triple3) -> (rule1 % int1))
Harry is not blue.
("Harry" "is" "blue" "-")
int1
Harry is blue.
False
2
inv-proof
[(((triple3) -> rule1))]
("Harry" "is" "blue" "+")
((triple3) -> (rule1 % int1))
Harry is not blue.
("Harry" "is" "blue" "-")
int1
Harry is quiet.
True
4
proof
[(((triple3 ((triple3) -> rule1)) -> rule3))]
("Harry" "is" "quiet" "+")
((triple3 ((triple3) -> (rule1 % int2))) -> (rule3 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is not blue.
("Harry" "is" "blue" "-")
int2
Harry is not quiet.
False
4
inv-proof
[(((triple3 ((triple3) -> rule1)) -> rule3))]
("Harry" "is" "quiet" "-")
((triple3 ((triple3) -> (rule1 % int2))) -> (rule3 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is not blue.
("Harry" "is" "blue" "-")
int2
Harry is smart.
True
6
proof
[(((((triple3 ((triple3) -> rule1)) -> rule3) triple3) -> rule4))]
("Harry" "is" "smart" "+")
((((triple3 ((triple3) -> (rule1 % int3))) -> (rule3 % int2)) triple3) -> (rule4 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is not blue.
("Harry" "is" "blue" "-")
int3
Harry is not smart.
False
6
inv-proof
[(((((triple3 ((triple3) -> rule1)) -> rule3) triple3) -> rule4))]
("Harry" "is" "smart" "-")
((((triple3 ((triple3) -> (rule1 % int3))) -> (rule3 % int2)) triple3) -> (rule4 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is not blue.
("Harry" "is" "blue" "-")
int3
Gary is not white.
Unknown
inv-rconc
[@2: Gary is white.[CWA. Example of deepest failure = (rule6 <- rule3 <- FAIL)]]
("Gary" "is" "white" "-")
Gary is smart.
Unknown
rconc
[@1: Gary is smart.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Gary" "is" "smart" "+")
Charlie is not smart.
Unknown
inv-rconc
[@1: Charlie is smart.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Charlie" "is" "smart" "-")
Gary is quiet.
Unknown
rconc
[@1: Gary is quiet.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "quiet" "+")
Charlie is not blue.
Unknown
inv-random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "-")
Harry is white.
Unknown
random
[@0: Harry is white.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "white" "+")
Charlie is not kind.
Unknown
inv-random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "-")
Gary is blue.
Unknown
random
[@0: Gary is blue.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "blue" "+")
@0: Charlie is nice.[(triple1)] Gary is nice.[(triple2)] Harry is kind.[(triple3)] @1: Harry is not blue.[(((triple3) -> rule1))] @2: Harry is quiet.[(((triple3 ((triple3) -> rule1)) -> rule3))] @3: Harry is smart.[(((((triple3 ((triple3) -> rule1)) -> rule3) triple3) -> rule4))]
Charlie is nice.
("Charlie" "is" "nice" "+")
triple1
Gary is nice.
("Gary" "is" "nice" "+")
triple2
Harry is kind.
("Harry" "is" "kind" "+")
triple3
Harry is not blue.
("Harry" "is" "blue" "-")
((triple3) -> (rule1 % int1))
Harry is not blue.
("Harry" "is" "blue" "-")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple3 ((triple3) -> (rule1 % int2))) -> (rule3 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is not blue.
("Harry" "is" "blue" "-")
int2
Harry is smart.
("Harry" "is" "smart" "+")
((((triple3 ((triple3) -> (rule1 % int3))) -> (rule3 % int2)) triple3) -> (rule4 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is not blue.
("Harry" "is" "blue" "-")
int3