Anne is red. Charlie is quiet. Harry is smart. Smart things are blue. Red things are smart. If something is rough then it is quiet.
Anne is red.
("Anne" "is" "red" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Smart things are blue.
((("something" "is" "smart" "+")) -> ("something" "is" "blue" "+"))
Red things are smart.
((("something" "is" "red" "+")) -> ("something" "is" "smart" "+"))
If something is rough then it is quiet.
((("something" "is" "rough" "+")) -> ("something" "is" "quiet" "+"))
Charlie is quiet.
True
1
proof
[(triple2)]
("Charlie" "is" "quiet" "+")
triple2
Harry is not smart.
False
1
inv-proof
[(triple3)]
("Harry" "is" "smart" "-")
triple3
Anne is smart.
True
2
proof
[(((triple1) -> rule2))]
("Anne" "is" "smart" "+")
((triple1) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Harry is not blue.
False
2
inv-proof
[(((triple3) -> rule1))]
("Harry" "is" "blue" "-")
((triple3) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Anne is blue.
True
3
proof
[(((((triple1) -> rule2)) -> rule1))]
("Anne" "is" "blue" "+")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is not blue.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule1))]
("Anne" "is" "blue" "-")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Harry is not quiet.
Unknown
inv-rconc
[@1: Harry is quiet.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "quiet" "-")
Anne is quiet.
Unknown
rconc
[@1: Anne is quiet.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Anne" "is" "quiet" "+")
Charlie is not blue.
Unknown
inv-rconc
[@2: Charlie is blue.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("Charlie" "is" "blue" "-")
Charlie is red.
Unknown
random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "+")
Harry is not big.
Unknown
inv-random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "-")
Charlie is white.
Unknown
random
[@0: Charlie is white.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "white" "+")
@0: Anne is red.[(triple1)] Charlie is quiet.[(triple2)] Harry is smart.[(triple3)] @1: Anne is smart.[(((triple1) -> rule2))] Harry is blue.[(((triple3) -> rule1))] @2: Anne is blue.[(((((triple1) -> rule2)) -> rule1))]
Anne is red.
("Anne" "is" "red" "+")
triple1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple2
Harry is smart.
("Harry" "is" "smart" "+")
triple3
Anne is smart.
("Anne" "is" "smart" "+")
((triple1) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
((triple3) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2