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