Anne is white. Charlie is quiet. Gary is young. Harry is blue. If something is smart and white then it is blue. All blue things are quiet. All furry, green things are blue. If something is smart then it is furry. If Anne is white then Anne is smart. Young, green things are blue. If Charlie is green and Charlie is young then Charlie is quiet. If something is blue then it is green.
Anne is white.
("Anne" "is" "white" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Gary is young.
("Gary" "is" "young" "+")
Harry is blue.
("Harry" "is" "blue" "+")
If something is smart and white then it is blue.
((("something" "is" "smart" "+") ("something" "is" "white" "+")) -> ("something" "is" "blue" "+"))
All blue things are quiet.
((("something" "is" "blue" "+")) -> ("something" "is" "quiet" "+"))
All furry, green things are blue.
((("something" "is" "furry" "+") ("something" "is" "green" "+")) -> ("something" "is" "blue" "+"))
If something is smart then it is furry.
((("something" "is" "smart" "+")) -> ("something" "is" "furry" "+"))
If Anne is white then Anne is smart.
((("Anne" "is" "white" "+")) -> ("Anne" "is" "smart" "+"))
Young, green things are blue.
((("something" "is" "young" "+") ("something" "is" "green" "+")) -> ("something" "is" "blue" "+"))
If Charlie is green and Charlie is young then Charlie is quiet.
((("Charlie" "is" "green" "+") ("Charlie" "is" "young" "+")) -> ("Charlie" "is" "quiet" "+"))
If something is blue then it is green.
((("something" "is" "blue" "+")) -> ("something" "is" "green" "+"))
Charlie is quiet.
True
1
proof
[(triple2)]
("Charlie" "is" "quiet" "+")
triple2
Charlie is not quiet.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "quiet" "-")
triple2
Anne is smart.
True
2
proof
[(((triple1) -> rule5))]
("Anne" "is" "smart" "+")
((triple1) -> (rule5 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is not smart.
False
2
inv-proof
[(((triple1) -> rule5))]
("Anne" "is" "smart" "-")
((triple1) -> (rule5 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is blue.
True
4
proof
[(((((triple1) -> rule5) triple1) -> rule1))]
("Anne" "is" "blue" "+")
((((triple1) -> (rule5 % int2)) triple1) -> (rule1 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is not blue.
False
4
inv-proof
[(((((triple1) -> rule5) triple1) -> rule1))]
("Anne" "is" "blue" "-")
((((triple1) -> (rule5 % int2)) triple1) -> (rule1 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is quiet.
True
5
proof
[(((((((triple1) -> rule5) triple1) -> rule1)) -> rule2))]
("Anne" "is" "quiet" "+")
((((((triple1) -> (rule5 % int3)) triple1) -> (rule1 % int2))) -> (rule2 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Anne is not green.
False
5
inv-proof
[(((((((triple1) -> rule5) triple1) -> rule1)) -> rule8))]
("Anne" "is" "green" "-")
((((((triple1) -> (rule5 % int3)) triple1) -> (rule1 % int2))) -> (rule8 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Gary is not blue.
Unknown
inv-rconc
[@3: Gary is blue.[CWA. Example of deepest failure = (rule6 <- rule8 <- rule1 <- FAIL)]]
("Gary" "is" "blue" "-")
Gary is green.
Unknown
rconc
[@2: Gary is green.[CWA. Example of deepest failure = (rule8 <- rule1 <- FAIL)]]
("Gary" "is" "green" "+")
Charlie is not furry.
Unknown
inv-rconc
[@1: Charlie is furry.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Charlie" "is" "furry" "-")
Charlie is blue.
Unknown
rconc
[@2: Charlie is blue.[CWA. Example of deepest failure = (rule3 <- rule4 <- FAIL)]]
("Charlie" "is" "blue" "+")
Charlie is not young.
Unknown
inv-random
[@0: Charlie is young.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "young" "-")
Harry is young.
Unknown
random
[@0: Harry is young.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "young" "+")
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 white.[(triple1)] Charlie is quiet.[(triple2)] Gary is young.[(triple3)] Harry is blue.[(triple4)] @1: Anne is smart.[(((triple1) -> rule5))] Harry is green.[(((triple4) -> rule8))] Harry is quiet.[(((triple4) -> rule2))] @2: Anne is blue.[(((((triple1) -> rule5) triple1) -> rule1))] Anne is furry.[(((((triple1) -> rule5)) -> rule4))] @3: Anne is green.[(((((((triple1) -> rule5) triple1) -> rule1)) -> rule8))] Anne is quiet.[(((((((triple1) -> rule5) triple1) -> rule1)) -> rule2))]
Anne is white.
("Anne" "is" "white" "+")
triple1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple2
Gary is young.
("Gary" "is" "young" "+")
triple3
Harry is blue.
("Harry" "is" "blue" "+")
triple4
Anne is smart.
("Anne" "is" "smart" "+")
((triple1) -> (rule5 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
((triple4) -> (rule8 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple4) -> (rule2 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
((((triple1) -> (rule5 % int2)) triple1) -> (rule1 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
((((triple1) -> (rule5 % int2))) -> (rule4 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
((((((triple1) -> (rule5 % int3)) triple1) -> (rule1 % int2))) -> (rule8 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Anne is quiet.
("Anne" "is" "quiet" "+")
((((((triple1) -> (rule5 % int3)) triple1) -> (rule1 % int2))) -> (rule2 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3