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