Anne is cold. Bob is cold. Harry is blue. If something is blue then it is young. If something is smart then it is blue. If something is cold then it is big.
Anne is cold.
("Anne" "is" "cold" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Harry is blue.
("Harry" "is" "blue" "+")
If something is blue then it is young.
((("something" "is" "blue" "+")) -> ("something" "is" "young" "+"))
If something is smart then it is blue.
((("something" "is" "smart" "+")) -> ("something" "is" "blue" "+"))
If something is cold then it is big.
((("something" "is" "cold" "+")) -> ("something" "is" "big" "+"))
Bob is cold.
True
1
proof
[(triple2)]
("Bob" "is" "cold" "+")
triple2
Anne is not cold.
False
1
inv-proof
[(triple1)]
("Anne" "is" "cold" "-")
triple1
Harry is young.
True
2
proof
[(((triple3) -> rule1))]
("Harry" "is" "young" "+")
((triple3) -> (rule1 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Anne is not big.
False
2
inv-proof
[(((triple1) -> rule3))]
("Anne" "is" "big" "-")
((triple1) -> (rule3 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is not blue.
Unknown
inv-rconc
[@1: Anne is blue.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "blue" "-")
Anne is young.
Unknown
rconc
[@2: Anne is young.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("Anne" "is" "young" "+")
Bob is not round.
Unknown
inv-random
[@0: Bob is round.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "round" "-")
Anne is smart.
Unknown
random
[@0: Anne is smart.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "smart" "+")
@0: Anne is cold.[(triple1)] Bob is cold.[(triple2)] Harry is blue.[(triple3)] @1: Anne is big.[(((triple1) -> rule3))] Bob is big.[(((triple2) -> rule3))] Harry is young.[(((triple3) -> rule1))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Bob is cold.
("Bob" "is" "cold" "+")
triple2
Harry is blue.
("Harry" "is" "blue" "+")
triple3
Anne is big.
("Anne" "is" "big" "+")
((triple1) -> (rule3 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
((triple2) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
((triple3) -> (rule1 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1