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