Anne is round. Charlie is kind. Dave is round. Erin is not kind. If Charlie is furry then Charlie is white. If someone is white and not smart then they are not blue. If someone is furry then they are not nice. All kind people are furry. If someone is white and not furry then they are round. If someone is kind and white then they are round.
Anne is round.
("Anne" "is" "round" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Dave is round.
("Dave" "is" "round" "+")
Erin is not kind.
("Erin" "is" "kind" "-")
If Charlie is furry then Charlie is white.
((("Charlie" "is" "furry" "+")) -> ("Charlie" "is" "white" "+"))
If someone is white and not smart then they are not blue.
((("someone" "is" "white" "+") ("someone" "is" "smart" "~")) -> ("someone" "is" "blue" "-"))
If someone is furry then they are not nice.
((("someone" "is" "furry" "+")) -> ("someone" "is" "nice" "-"))
All kind people are furry.
((("someone" "is" "kind" "+")) -> ("someone" "is" "furry" "+"))
If someone is white and not furry then they are round.
((("someone" "is" "white" "+") ("someone" "is" "furry" "~")) -> ("someone" "is" "round" "+"))
If someone is kind and white then they are round.
((("someone" "is" "kind" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "round" "+"))
Charlie is kind.
True
1
proof
[(triple2)]
("Charlie" "is" "kind" "+")
triple2
Erin is kind.
False
1
inv-proof
[(triple4)]
("Erin" "is" "kind" "+")
triple4
Charlie is furry.
True
2
proof
[(((triple2) -> rule4))]
("Charlie" "is" "furry" "+")
((triple2) -> (rule4 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is not furry.
False
2
inv-proof
[(((triple2) -> rule4))]
("Charlie" "is" "furry" "-")
((triple2) -> (rule4 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is not nice.
True
3
proof
[(((((triple2) -> rule4)) -> rule3))]
("Charlie" "is" "nice" "-")
((((triple2) -> (rule4 % int2))) -> (rule3 % int1))
Charlie is not nice.
("Charlie" "is" "nice" "-")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is not white.
False
3
inv-proof
[(((((triple2) -> rule4)) -> rule1))]
("Charlie" "is" "white" "-")
((((triple2) -> (rule4 % int2))) -> (rule1 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is round.
True
5
proof
[(((triple2 ((((triple2) -> rule4)) -> rule1)) -> rule6))]
("Charlie" "is" "round" "+")
((triple2 ((((triple2) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3
Charlie is not round.
False
5
inv-proof
[(((triple2 ((((triple2) -> rule4)) -> rule1)) -> rule6))]
("Charlie" "is" "round" "-")
((triple2 ((((triple2) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3
Dave is not furry.
Unknown
inv-rconc
[@1: Dave is furry.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Dave" "is" "furry" "-")
Erin is furry.
Unknown
rconc
[@1: Erin is furry.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Erin" "is" "furry" "+")
Erin is not round.
Unknown
inv-rconc
[@1: Erin is round.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Erin" "is" "round" "-")
Anne is furry.
Unknown
rconc
[@1: Anne is furry.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Anne" "is" "furry" "+")
Anne is not kind.
Unknown
inv-random
[@0: Anne is kind.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "kind" "-")
Erin is nice.
Unknown
random
[@0: Erin is nice.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "nice" "+")
Dave is not white.
Unknown
inv-random
[@0: Dave is white.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "white" "-")
Charlie is smart.
Unknown
random
[@0: Charlie is smart.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "smart" "+")
@0: Anne is round.[(triple1)] Charlie is kind.[(triple2)] Dave is round.[(triple3)] Erin is not kind.[(triple4)] @1: Charlie is furry.[(((triple2) -> rule4))] @2: Charlie is not nice.[(((((triple2) -> rule4)) -> rule3))] Charlie is white.[(((((triple2) -> rule4)) -> rule1))] @3: Charlie is round.[(((triple2 ((((triple2) -> rule4)) -> rule1)) -> rule6))]
Anne is round.
("Anne" "is" "round" "+")
triple1
Charlie is kind.
("Charlie" "is" "kind" "+")
triple2
Dave is round.
("Dave" "is" "round" "+")
triple3
Erin is not kind.
("Erin" "is" "kind" "-")
triple4
Charlie is furry.
("Charlie" "is" "furry" "+")
((triple2) -> (rule4 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is not nice.
("Charlie" "is" "nice" "-")
((((triple2) -> (rule4 % int2))) -> (rule3 % int1))
Charlie is not nice.
("Charlie" "is" "nice" "-")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
((((triple2) -> (rule4 % int2))) -> (rule1 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
((triple2 ((((triple2) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3