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