Anne is round. Dave is nice. All furry things are nice. Furry things are smart. If something is young then it is green. All young, white things are nice. Round things are furry. All smart, furry things are young. If something is white then it is smart. All white, young things are nice.
Anne is round.
("Anne" "is" "round" "+")
Dave is nice.
("Dave" "is" "nice" "+")
All furry things are nice.
((("something" "is" "furry" "+")) -> ("something" "is" "nice" "+"))
Furry things are smart.
((("something" "is" "furry" "+")) -> ("something" "is" "smart" "+"))
If something is young then it is green.
((("something" "is" "young" "+")) -> ("something" "is" "green" "+"))
All young, white things are nice.
((("something" "is" "young" "+") ("something" "is" "white" "+")) -> ("something" "is" "nice" "+"))
Round things are furry.
((("something" "is" "round" "+")) -> ("something" "is" "furry" "+"))
All smart, furry things are young.
((("something" "is" "smart" "+") ("something" "is" "furry" "+")) -> ("something" "is" "young" "+"))
If something is white then it is smart.
((("something" "is" "white" "+")) -> ("something" "is" "smart" "+"))
All white, young things are nice.
((("something" "is" "white" "+") ("something" "is" "young" "+")) -> ("something" "is" "nice" "+"))
Dave is nice.
True
1
proof
[(triple2)]
("Dave" "is" "nice" "+")
triple2
Dave is not nice.
False
1
inv-proof
[(triple2)]
("Dave" "is" "nice" "-")
triple2
Anne is furry.
True
2
proof
[(((triple1) -> rule5))]
("Anne" "is" "furry" "+")
((triple1) -> (rule5 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is not furry.
False
2
inv-proof
[(((triple1) -> rule5))]
("Anne" "is" "furry" "-")
((triple1) -> (rule5 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is nice.
True
3
proof
[(((((triple1) -> rule5)) -> rule1))]
("Anne" "is" "nice" "+")
((((triple1) -> (rule5 % int2))) -> (rule1 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is not nice.
False
3
inv-proof
[(((((triple1) -> rule5)) -> rule1))]
("Anne" "is" "nice" "-")
((((triple1) -> (rule5 % int2))) -> (rule1 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is young.
True
6
proof
[(((((((triple1) -> rule5)) -> rule2) ((triple1) -> rule5)) -> rule6))]
("Anne" "is" "young" "+")
((((((triple1) -> (rule5 % int3))) -> (rule2 % int2)) ((triple1) -> (rule5 % int3))) -> (rule6 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Anne is not young.
False
6
inv-proof
[(((((((triple1) -> rule5)) -> rule2) ((triple1) -> rule5)) -> rule6))]
("Anne" "is" "young" "-")
((((((triple1) -> (rule5 % int3))) -> (rule2 % int2)) ((triple1) -> (rule5 % int3))) -> (rule6 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Dave is not young.
Unknown
inv-rconc
[@2: Dave is young.[CWA. Example of deepest failure = (rule6 <- rule5 <- FAIL)]]
("Dave" "is" "young" "-")
Dave is furry.
Unknown
rconc
[@1: Dave is furry.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Dave" "is" "furry" "+")
Dave is not green.
Unknown
inv-rconc
[@3: Dave is green.[CWA. Example of deepest failure = (rule3 <- rule6 <- rule5 <- FAIL)]]
("Dave" "is" "green" "-")
Dave is smart.
Unknown
rconc
[@2: Dave is smart.[CWA. Example of deepest failure = (rule2 <- rule5 <- FAIL)]]
("Dave" "is" "smart" "+")
Dave is not round.
Unknown
inv-random
[@0: Dave is round.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "round" "-")
Anne is white.
Unknown
random
[@0: Anne is white.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "white" "+")
@0: Anne is round.[(triple1)] Dave is nice.[(triple2)] @1: Anne is furry.[(((triple1) -> rule5))] @2: Anne is nice.[(((((triple1) -> rule5)) -> rule1))] Anne is smart.[(((((triple1) -> rule5)) -> rule2))] @3: Anne is young.[(((((((triple1) -> rule5)) -> rule2) ((triple1) -> rule5)) -> rule6))] @4: Anne is green.[(((((((((triple1) -> rule5)) -> rule2) ((triple1) -> rule5)) -> rule6)) -> rule3))]
Anne is round.
("Anne" "is" "round" "+")
triple1
Dave is nice.
("Dave" "is" "nice" "+")
triple2
Anne is furry.
("Anne" "is" "furry" "+")
((triple1) -> (rule5 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
((((triple1) -> (rule5 % int2))) -> (rule1 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
((((triple1) -> (rule5 % int2))) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
((((((triple1) -> (rule5 % int3))) -> (rule2 % int2)) ((triple1) -> (rule5 % int3))) -> (rule6 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Anne is green.
("Anne" "is" "green" "+")
((((((((triple1) -> (rule5 % int4))) -> (rule2 % int3)) ((triple1) -> (rule5 % int4))) -> (rule6 % int2))) -> (rule3 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Anne is furry.
("Anne" "is" "furry" "+")
int4