Anne is not cold. Anne is kind. Bob is cold. Bob is not round. Bob is white. Erin is kind. Erin is quiet. Erin is round. Erin is white. Gary is not round. If someone is quiet then they are not furry. If someone is quiet and not cold then they are furry. All nice people are furry. All cold people are nice. Round, cold people are nice. If someone is round and not cold then they are not nice. If someone is nice and furry then they are kind. All quiet people are round.
Anne is not cold.
("Anne" "is" "cold" "-")
Anne is kind.
("Anne" "is" "kind" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is not round.
("Bob" "is" "round" "-")
Bob is white.
("Bob" "is" "white" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is white.
("Erin" "is" "white" "+")
Gary is not round.
("Gary" "is" "round" "-")
If someone is quiet then they are not furry.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "furry" "-"))
If someone is quiet and not cold then they are furry.
((("someone" "is" "quiet" "+") ("someone" "is" "cold" "~")) -> ("someone" "is" "furry" "+"))
All nice people are furry.
((("someone" "is" "nice" "+")) -> ("someone" "is" "furry" "+"))
All cold people are nice.
((("someone" "is" "cold" "+")) -> ("someone" "is" "nice" "+"))
Round, cold people are nice.
((("someone" "is" "round" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "nice" "+"))
If someone is round and not cold then they are not nice.
((("someone" "is" "round" "+") ("someone" "is" "cold" "~")) -> ("someone" "is" "nice" "-"))
If someone is nice and furry then they are kind.
((("someone" "is" "nice" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "kind" "+"))
All quiet people are round.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "round" "+"))
Bob is cold.
True
1
proof
[(triple3)]
("Bob" "is" "cold" "+")
triple3
Bob is not white.
False
1
inv-proof
[(triple5)]
("Bob" "is" "white" "-")
triple5
Bob is nice.
True
2
proof
[(((triple3) -> rule4))]
("Bob" "is" "nice" "+")
((triple3) -> (rule4 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Erin is furry.
False
2
inv-proof
[(((triple7) -> rule1))]
("Erin" "is" "furry" "+")
((triple7) -> (rule1 % int1))
Erin is not furry.
("Erin" "is" "furry" "-")
int1
Bob is furry.
True
3
proof
[(((((triple3) -> rule4)) -> rule3))]
("Bob" "is" "furry" "+")
((((triple3) -> (rule4 % int2))) -> (rule3 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is not furry.
False
3
inv-proof
[(((((triple3) -> rule4)) -> rule3))]
("Bob" "is" "furry" "-")
((((triple3) -> (rule4 % int2))) -> (rule3 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is kind.
True
6
proof
[(((((triple3) -> rule4) ((((triple3) -> rule4)) -> rule3)) -> rule7))]
("Bob" "is" "kind" "+")
((((triple3) -> (rule4 % int3)) ((((triple3) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
int3
Bob is not kind.
False
6
inv-proof
[(((((triple3) -> rule4) ((((triple3) -> rule4)) -> rule3)) -> rule7))]
("Bob" "is" "kind" "-")
((((triple3) -> (rule4 % int3)) ((((triple3) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
int3
Gary is not kind.
Unknown
inv-rconc
[@2: Gary is kind.[CWA. Example of deepest failure = (rule7 <- rule4 <- FAIL)]]
("Gary" "is" "kind" "-")
Anne is round.
Unknown
rconc
[@1: Anne is round.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Anne" "is" "round" "+")
Anne is not furry.
Unknown
inv-rconc
[@2: Anne is furry.[CWA. Example of deepest failure = (rule3 <- rule4 <- FAIL)]]
("Anne" "is" "furry" "-")
Erin is nice.
Unknown
rconc
[@1: Erin is nice.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Erin" "is" "nice" "+")
Erin is not cold.
Unknown
inv-random
[@0: Erin is cold.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "cold" "-")
Gary is cold.
Unknown
random
[@0: Gary is cold.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "cold" "+")
Gary is not white.
Unknown
inv-random
[@0: Gary is white.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "white" "-")
Gary is quiet.
Unknown
random
[@0: Gary is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "quiet" "+")
@0: Anne is kind.[(triple2)] Anne is not cold.[(triple1)] Bob is cold.[(triple3)] Bob is not round.[(triple4)] Bob is white.[(triple5)] Erin is kind.[(triple6)] Erin is quiet.[(triple7)] Erin is round.[(triple8 OR ((triple7) -> rule8))] Erin is white.[(triple9)] Gary is not round.[(triple10)] @1: Bob is nice.[(((triple3) -> rule4))] Erin is not furry.[(((triple7) -> rule1))] @2: Bob is furry.[(((((triple3) -> rule4)) -> rule3))] @3: Bob is kind.[(((((triple3) -> rule4) ((((triple3) -> rule4)) -> rule3)) -> rule7))]
Anne is kind.
("Anne" "is" "kind" "+")
triple2
Anne is not cold.
("Anne" "is" "cold" "-")
triple1
Bob is cold.
("Bob" "is" "cold" "+")
triple3
Bob is not round.
("Bob" "is" "round" "-")
triple4
Bob is white.
("Bob" "is" "white" "+")
triple5
Erin is kind.
("Erin" "is" "kind" "+")
triple6
Erin is quiet.
("Erin" "is" "quiet" "+")
triple7
Erin is round.
("Erin" "is" "round" "+")
triple8
((triple7) -> (rule8 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
triple9
Gary is not round.
("Gary" "is" "round" "-")
triple10
Bob is nice.
("Bob" "is" "nice" "+")
((triple3) -> (rule4 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Erin is not furry.
("Erin" "is" "furry" "-")
((triple7) -> (rule1 % int1))
Erin is not furry.
("Erin" "is" "furry" "-")
int1
Bob is furry.
("Bob" "is" "furry" "+")
((((triple3) -> (rule4 % int2))) -> (rule3 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
((((triple3) -> (rule4 % int3)) ((((triple3) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
int3