Bob is smart. Erin is kind. Gary is kind. Harry is round. If Harry is young and Harry is blue then Harry is green. Blue, green things are kind. If something is young then it is red. If something is round then it is blue. Red things are young. If something is blue then it is kind.
Bob is smart.
("Bob" "is" "smart" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Harry is round.
("Harry" "is" "round" "+")
If Harry is young and Harry is blue then Harry is green.
((("Harry" "is" "young" "+") ("Harry" "is" "blue" "+")) -> ("Harry" "is" "green" "+"))
Blue, green things are kind.
((("something" "is" "blue" "+") ("something" "is" "green" "+")) -> ("something" "is" "kind" "+"))
If something is young then it is red.
((("something" "is" "young" "+")) -> ("something" "is" "red" "+"))
If something is round then it is blue.
((("something" "is" "round" "+")) -> ("something" "is" "blue" "+"))
Red things are young.
((("something" "is" "red" "+")) -> ("something" "is" "young" "+"))
If something is blue then it is kind.
((("something" "is" "blue" "+")) -> ("something" "is" "kind" "+"))
Erin is kind.
True
1
proof
[(triple2)]
("Erin" "is" "kind" "+")
triple2
Harry is not round.
False
1
inv-proof
[(triple4)]
("Harry" "is" "round" "-")
triple4
Harry is blue.
True
2
proof
[(((triple4) -> rule4))]
("Harry" "is" "blue" "+")
((triple4) -> (rule4 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is not blue.
False
2
inv-proof
[(((triple4) -> rule4))]
("Harry" "is" "blue" "-")
((triple4) -> (rule4 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Bob is not kind.
Unknown
inv-rconc
[@2: Bob is kind.[CWA. Example of deepest failure = (rule6 <- rule4 <- FAIL)]]
("Bob" "is" "kind" "-")
Harry is young.
Unknown
rconc
[@2: Harry is young.[CWA. Example of deepest failure = (rule5 <- rule3 <- FAIL)]]
("Harry" "is" "young" "+")
Harry is not smart.
Unknown
inv-random
[@0: Harry is smart.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "smart" "-")
Gary is green.
Unknown
random
[@0: Gary is green.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "green" "+")
@0: Bob is smart.[(triple1)] Erin is kind.[(triple2)] Gary is kind.[(triple3)] Harry is round.[(triple4)] @1: Harry is blue.[(((triple4) -> rule4))] @2: Harry is kind.[(((((triple4) -> rule4)) -> rule6))]
Bob is smart.
("Bob" "is" "smart" "+")
triple1
Erin is kind.
("Erin" "is" "kind" "+")
triple2
Gary is kind.
("Gary" "is" "kind" "+")
triple3
Harry is round.
("Harry" "is" "round" "+")
triple4
Harry is blue.
("Harry" "is" "blue" "+")
((triple4) -> (rule4 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
((((triple4) -> (rule4 % int2))) -> (rule6 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2