Anne is rough. Charlie is nice. Dave is young. If Charlie is round and Charlie is young then Charlie is big. Round things are white. All rough things are young.
Anne is rough.
("Anne" "is" "rough" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Dave is young.
("Dave" "is" "young" "+")
If Charlie is round and Charlie is young then Charlie is big.
((("Charlie" "is" "round" "+") ("Charlie" "is" "young" "+")) -> ("Charlie" "is" "big" "+"))
Round things are white.
((("something" "is" "round" "+")) -> ("something" "is" "white" "+"))
All rough things are young.
((("something" "is" "rough" "+")) -> ("something" "is" "young" "+"))
Charlie is nice.
True
1
proof
[(triple2)]
("Charlie" "is" "nice" "+")
triple2
Charlie is not nice.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "nice" "-")
triple2
Anne is young.
True
2
proof
[(((triple1) -> rule3))]
("Anne" "is" "young" "+")
((triple1) -> (rule3 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is not young.
False
2
inv-proof
[(((triple1) -> rule3))]
("Anne" "is" "young" "-")
((triple1) -> (rule3 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Charlie is not white.
Unknown
inv-rconc
[@1: Charlie is white.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "white" "-")
Dave is white.
Unknown
rconc
[@1: Dave is white.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "white" "+")
Dave is not red.
Unknown
inv-random
[@0: Dave is red.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "red" "-")
Anne is big.
Unknown
random
[@0: Anne is big.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "big" "+")
@0: Anne is rough.[(triple1)] Charlie is nice.[(triple2)] Dave is young.[(triple3)] @1: Anne is young.[(((triple1) -> rule3))]
Anne is rough.
("Anne" "is" "rough" "+")
triple1
Charlie is nice.
("Charlie" "is" "nice" "+")
triple2
Dave is young.
("Dave" "is" "young" "+")
triple3
Anne is young.
("Anne" "is" "young" "+")
((triple1) -> (rule3 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1