Anne is green. Anne is smart. Charlie is blue. Charlie is red. Charlie is round. Charlie is young. Harry is blue. Harry is green. Harry is kind. Harry is round. If something is green then it is blue. If something is green and smart then it is kind.
Anne is green.
("Anne" "is" "green" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is round.
("Harry" "is" "round" "+")
If something is green then it is blue.
((("something" "is" "green" "+")) -> ("something" "is" "blue" "+"))
If something is green and smart then it is kind.
((("something" "is" "green" "+") ("something" "is" "smart" "+")) -> ("something" "is" "kind" "+"))
Charlie is red.
True
1
proof
[(triple4)]
("Charlie" "is" "red" "+")
triple4
Harry is not kind.
False
1
inv-proof
[(triple9)]
("Harry" "is" "kind" "-")
triple9
Charlie is not kind.
Unknown
inv-rconc
[@1: Charlie is kind.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "kind" "-")
Charlie is smart.
Unknown
random
[@0: Charlie is smart.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "smart" "+")
@0: Anne is green.[(triple1)] Anne is smart.[(triple2)] Charlie is blue.[(triple3)] Charlie is red.[(triple4)] Charlie is round.[(triple5)] Charlie is young.[(triple6)] Harry is blue.[(triple7 OR ((triple8) -> rule1))] Harry is green.[(triple8)] Harry is kind.[(triple9)] Harry is round.[(triple10)] @1: Anne is blue.[(((triple1) -> rule1))] Anne is kind.[(((triple1 triple2) -> rule2))]
Anne is green.
("Anne" "is" "green" "+")
triple1
Anne is smart.
("Anne" "is" "smart" "+")
triple2
Charlie is blue.
("Charlie" "is" "blue" "+")
triple3
Charlie is red.
("Charlie" "is" "red" "+")
triple4
Charlie is round.
("Charlie" "is" "round" "+")
triple5
Charlie is young.
("Charlie" "is" "young" "+")
triple6
Harry is blue.
("Harry" "is" "blue" "+")
triple7
((triple8) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
triple8
Harry is kind.
("Harry" "is" "kind" "+")
triple9
Harry is round.
("Harry" "is" "round" "+")
triple10
Anne is blue.
("Anne" "is" "blue" "+")
((triple1) -> (rule1 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
((triple1 triple2) -> (rule2 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1