Anne is not nice. Dave is smart. Gary is young. Smart, green things are furry. All smart things are quiet. If Dave is furry and Dave is not young then Dave is round. If something is quiet then it is green. All quiet, young things are green. If Gary is green and Gary is nice then Gary is not furry.
Anne is not nice.
("Anne" "is" "nice" "-")
Dave is smart.
("Dave" "is" "smart" "+")
Gary is young.
("Gary" "is" "young" "+")
Smart, green things are furry.
((("something" "is" "smart" "+") ("something" "is" "green" "+")) -> ("something" "is" "furry" "+"))
All smart things are quiet.
((("something" "is" "smart" "+")) -> ("something" "is" "quiet" "+"))
If Dave is furry and Dave is not young then Dave is round.
((("Dave" "is" "furry" "+") ("Dave" "is" "young" "~")) -> ("Dave" "is" "round" "+"))
If something is quiet then it is green.
((("something" "is" "quiet" "+")) -> ("something" "is" "green" "+"))
All quiet, young things are green.
((("something" "is" "quiet" "+") ("something" "is" "young" "+")) -> ("something" "is" "green" "+"))
If Gary is green and Gary is nice then Gary is not furry.
((("Gary" "is" "green" "+") ("Gary" "is" "nice" "+")) -> ("Gary" "is" "furry" "-"))
Anne is not nice.
True
1
proof
[(triple1)]
("Anne" "is" "nice" "-")
triple1
Anne is nice.
False
1
inv-proof
[(triple1)]
("Anne" "is" "nice" "+")
triple1
Dave is quiet.
True
2
proof
[(((triple2) -> rule2))]
("Dave" "is" "quiet" "+")
((triple2) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is not quiet.
False
2
inv-proof
[(((triple2) -> rule2))]
("Dave" "is" "quiet" "-")
((triple2) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is green.
True
3
proof
[(((((triple2) -> rule2)) -> rule4))]
("Dave" "is" "green" "+")
((((triple2) -> (rule2 % int2))) -> (rule4 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is not green.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule4))]
("Dave" "is" "green" "-")
((((triple2) -> (rule2 % int2))) -> (rule4 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is furry.
True
5
proof
[(((triple2 ((((triple2) -> rule2)) -> rule4)) -> rule1))]
("Dave" "is" "furry" "+")
((triple2 ((((triple2) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Dave is not furry.
False
5
inv-proof
[(((triple2 ((((triple2) -> rule2)) -> rule4)) -> rule1))]
("Dave" "is" "furry" "-")
((triple2 ((((triple2) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Gary is not green.
Unknown
inv-rconc
[@2: Gary is green.[CWA. Example of deepest failure = (rule4 <- rule2 <- FAIL)]]
("Gary" "is" "green" "-")
Gary is furry.
Unknown
rconc
[@1: Gary is furry.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "furry" "+")
Anne is not furry.
Unknown
inv-rconc
[@1: Anne is furry.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "furry" "-")
Anne is quiet.
Unknown
rconc
[@1: Anne is quiet.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "quiet" "+")
Anne is not round.
Unknown
inv-random
[@0: Anne is round.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "round" "-")
Gary is smart.
Unknown
random
[@0: Gary is smart.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "smart" "+")
Anne is not smart.
Unknown
inv-random
[@0: Anne is smart.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "smart" "-")
Gary is round.
Unknown
random
[@0: Gary is round.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "round" "+")
@0: Anne is not nice.[(triple1)] Dave is smart.[(triple2)] Gary is young.[(triple3)] @1: Dave is quiet.[(((triple2) -> rule2))] @2: Dave is green.[(((((triple2) -> rule2)) -> rule4))] @3: Dave is furry.[(((triple2 ((((triple2) -> rule2)) -> rule4)) -> rule1))]
Anne is not nice.
("Anne" "is" "nice" "-")
triple1
Dave is smart.
("Dave" "is" "smart" "+")
triple2
Gary is young.
("Gary" "is" "young" "+")
triple3
Dave is quiet.
("Dave" "is" "quiet" "+")
((triple2) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
((((triple2) -> (rule2 % int2))) -> (rule4 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
((triple2 ((((triple2) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3