Anne is kind. Anne is smart. Anne is white. Dave is furry. Dave is smart. Gary is furry. Gary is nice. All big, white things are nice. All furry, nice things are round. If something is white then it is big.
Anne is kind.
("Anne" "is" "kind" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Anne is white.
("Anne" "is" "white" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is nice.
("Gary" "is" "nice" "+")
All big, white things are nice.
((("something" "is" "big" "+") ("something" "is" "white" "+")) -> ("something" "is" "nice" "+"))
All furry, nice things are round.
((("something" "is" "furry" "+") ("something" "is" "nice" "+")) -> ("something" "is" "round" "+"))
If something is white then it is big.
((("something" "is" "white" "+")) -> ("something" "is" "big" "+"))
Anne is smart.
True
1
proof
[(triple2)]
("Anne" "is" "smart" "+")
triple2
Anne is not smart.
False
1
inv-proof
[(triple2)]
("Anne" "is" "smart" "-")
triple2
Anne is big.
True
2
proof
[(((triple3) -> rule3))]
("Anne" "is" "big" "+")
((triple3) -> (rule3 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Gary is not round.
False
3
inv-proof
[(((triple6 triple7) -> rule2))]
("Gary" "is" "round" "-")
((triple6 triple7) -> (rule2 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Anne is nice.
True
4
proof
[(((((triple3) -> rule3) triple3) -> rule1))]
("Anne" "is" "nice" "+")
((((triple3) -> (rule3 % int2)) triple3) -> (rule1 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is not nice.
False
4
inv-proof
[(((((triple3) -> rule3) triple3) -> rule1))]
("Anne" "is" "nice" "-")
((((triple3) -> (rule3 % int2)) triple3) -> (rule1 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is not round.
Unknown
inv-rconc
[@1: Anne is round.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "round" "-")
Dave is round.
Unknown
rconc
[@2: Dave is round.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("Dave" "is" "round" "+")
Dave is not nice.
Unknown
inv-rconc
[@1: Dave is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "nice" "-")
Dave is kind.
Unknown
random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "+")
Gary is not white.
Unknown
inv-random
[@0: Gary is white.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "white" "-")
Gary is kind.
Unknown
random
[@0: Gary is kind.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "kind" "+")
@0: Anne is kind.[(triple1)] Anne is smart.[(triple2)] Anne is white.[(triple3)] Dave is furry.[(triple4)] Dave is smart.[(triple5)] Gary is furry.[(triple6)] Gary is nice.[(triple7)] @1: Anne is big.[(((triple3) -> rule3))] Gary is round.[(((triple6 triple7) -> rule2))] @2: Anne is nice.[(((((triple3) -> rule3) triple3) -> rule1))]
Anne is kind.
("Anne" "is" "kind" "+")
triple1
Anne is smart.
("Anne" "is" "smart" "+")
triple2
Anne is white.
("Anne" "is" "white" "+")
triple3
Dave is furry.
("Dave" "is" "furry" "+")
triple4
Dave is smart.
("Dave" "is" "smart" "+")
triple5
Gary is furry.
("Gary" "is" "furry" "+")
triple6
Gary is nice.
("Gary" "is" "nice" "+")
triple7
Anne is big.
("Anne" "is" "big" "+")
((triple3) -> (rule3 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
((triple6 triple7) -> (rule2 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
((((triple3) -> (rule3 % int2)) triple3) -> (rule1 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2