Anne is white. Charlie is blue. All smart, nice people are blue. Smart people are blue. Blue, nice people are smart. Nice people are young. If Charlie is white and Charlie is rough then Charlie is young. All white people are smart.
Anne is white.
("Anne" "is" "white" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
All smart, nice people are blue.
((("someone" "is" "smart" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "blue" "+"))
Smart people are blue.
((("someone" "is" "smart" "+")) -> ("someone" "is" "blue" "+"))
Blue, nice people are smart.
((("someone" "is" "blue" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "smart" "+"))
Nice people are young.
((("someone" "is" "nice" "+")) -> ("someone" "is" "young" "+"))
If Charlie is white and Charlie is rough then Charlie is young.
((("Charlie" "is" "white" "+") ("Charlie" "is" "rough" "+")) -> ("Charlie" "is" "young" "+"))
All white people are smart.
((("someone" "is" "white" "+")) -> ("someone" "is" "smart" "+"))
Anne is white.
True
1
proof
[(triple1)]
("Anne" "is" "white" "+")
triple1
Charlie is not blue.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "blue" "-")
triple2
Anne is smart.
True
2
proof
[(((triple1) -> rule6))]
("Anne" "is" "smart" "+")
((triple1) -> (rule6 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is not smart.
False
2
inv-proof
[(((triple1) -> rule6))]
("Anne" "is" "smart" "-")
((triple1) -> (rule6 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is blue.
True
3
proof
[(((((triple1) -> rule6)) -> rule2))]
("Anne" "is" "blue" "+")
((((triple1) -> (rule6 % int2))) -> (rule2 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is not blue.
False
3
inv-proof
[(((((triple1) -> rule6)) -> rule2))]
("Anne" "is" "blue" "-")
((((triple1) -> (rule6 % int2))) -> (rule2 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Charlie is not smart.
Unknown
inv-rconc
[@1: Charlie is smart.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "smart" "-")
Charlie is young.
Unknown
rconc
[@1: Charlie is young.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Charlie" "is" "young" "+")
Anne is not young.
Unknown
inv-rconc
[@1: Anne is young.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Anne" "is" "young" "-")
Anne is nice.
Unknown
random
[@0: Anne is nice.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "nice" "+")
Anne is not big.
Unknown
inv-random
[@0: Anne is big.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "big" "-")
Charlie is nice.
Unknown
random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "+")
@0: Anne is white.[(triple1)] Charlie is blue.[(triple2)] @1: Anne is smart.[(((triple1) -> rule6))] @2: Anne is blue.[(((((triple1) -> rule6)) -> rule2))]
Anne is white.
("Anne" "is" "white" "+")
triple1
Charlie is blue.
("Charlie" "is" "blue" "+")
triple2
Anne is smart.
("Anne" "is" "smart" "+")
((triple1) -> (rule6 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
((((triple1) -> (rule6 % int2))) -> (rule2 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2