Charlie is kind. Charlie is quiet. Charlie is red. Charlie is smart. Charlie is young. Dave is red. Dave is smart. If someone is red and not round then they are not quiet. All quiet people are furry.
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is smart.
("Dave" "is" "smart" "+")
If someone is red and not round then they are not quiet.
((("someone" "is" "red" "+") ("someone" "is" "round" "~")) -> ("someone" "is" "quiet" "-"))
All quiet people are furry.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "furry" "+"))
Charlie is smart.
True
1
proof
[(triple4)]
("Charlie" "is" "smart" "+")
triple4
Charlie is not young.
False
1
inv-proof
[(triple5)]
("Charlie" "is" "young" "-")
triple5
Charlie is furry.
True
2
proof
[(((triple2) -> rule2))]
("Charlie" "is" "furry" "+")
((triple2) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is not furry.
False
2
inv-proof
[(((triple2) -> rule2))]
("Charlie" "is" "furry" "-")
((triple2) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Dave is not furry.
Unknown
inv-rconc
[@1: Dave is furry.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "furry" "-")
Charlie is round.
Unknown
random
[@0: Charlie is round.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "round" "+")
Dave is not round.
Unknown
inv-random
[@0: Dave is round.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "round" "-")
Dave is quiet.
Unknown
random
[@0: Dave is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "quiet" "+")
@0: Charlie is kind.[(triple1)] Charlie is quiet.[(triple2)] Charlie is red.[(triple3)] Charlie is smart.[(triple4)] Charlie is young.[(triple5)] Dave is red.[(triple6)] Dave is smart.[(triple7)] @1: Charlie is furry.[(((triple2) -> rule2))]
Charlie is kind.
("Charlie" "is" "kind" "+")
triple1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple2
Charlie is red.
("Charlie" "is" "red" "+")
triple3
Charlie is smart.
("Charlie" "is" "smart" "+")
triple4
Charlie is young.
("Charlie" "is" "young" "+")
triple5
Dave is red.
("Dave" "is" "red" "+")
triple6
Dave is smart.
("Dave" "is" "smart" "+")
triple7
Charlie is furry.
("Charlie" "is" "furry" "+")
((triple2) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1