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