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