Anne is not smart. Bob is nice. Charlie is furry. Erin is nice. Furry people are not smart. If someone is nice then they are cold. If someone is cold and not young then they are nice. All nice people are furry. Young, nice people are not white. Nice people are white.
Anne is not smart.
("Anne" "is" "smart" "-")
Bob is nice.
("Bob" "is" "nice" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Furry people are not smart.
((("someone" "is" "furry" "+")) -> ("someone" "is" "smart" "-"))
If someone is nice then they are cold.
((("someone" "is" "nice" "+")) -> ("someone" "is" "cold" "+"))
If someone is cold and not young then they are nice.
((("someone" "is" "cold" "+") ("someone" "is" "young" "~")) -> ("someone" "is" "nice" "+"))
All nice people are furry.
((("someone" "is" "nice" "+")) -> ("someone" "is" "furry" "+"))
Young, nice people are not white.
((("someone" "is" "young" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "white" "-"))
Nice people are white.
((("someone" "is" "nice" "+")) -> ("someone" "is" "white" "+"))
Erin is nice.
True
1
proof
[(triple4)]
("Erin" "is" "nice" "+")
triple4
Charlie is not furry.
False
1
inv-proof
[(triple3)]
("Charlie" "is" "furry" "-")
triple3
Erin is white.
True
2
proof
[(((triple4) -> rule6))]
("Erin" "is" "white" "+")
((triple4) -> (rule6 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Charlie is smart.
False
2
inv-proof
[(((triple3) -> rule1))]
("Charlie" "is" "smart" "+")
((triple3) -> (rule1 % int1))
Charlie is not smart.
("Charlie" "is" "smart" "-")
int1
Bob is not smart.
True
3
proof
[(((((triple2) -> rule4)) -> rule1))]
("Bob" "is" "smart" "-")
((((triple2) -> (rule4 % int2))) -> (rule1 % int1))
Bob is not smart.
("Bob" "is" "smart" "-")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Erin is smart.
False
3
inv-proof
[(((((triple4) -> rule4)) -> rule1))]
("Erin" "is" "smart" "+")
((((triple4) -> (rule4 % int2))) -> (rule1 % int1))
Erin is not smart.
("Erin" "is" "smart" "-")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Anne is not furry.
Unknown
inv-rconc
[@2: Anne is furry.[CWA. Example of deepest failure = (rule4 <- rule3 <- FAIL)]]
("Anne" "is" "furry" "-")
Anne is nice.
Unknown
rconc
[@1: Anne is nice.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Anne" "is" "nice" "+")
Charlie is not white.
Unknown
inv-rconc
[@2: Charlie is white.[CWA. Example of deepest failure = (rule6 <- rule3 <- FAIL)]]
("Charlie" "is" "white" "-")
Charlie is quiet.
Unknown
random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "+")
Erin is not young.
Unknown
inv-random
[@0: Erin is young.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "young" "-")
Bob is quiet.
Unknown
random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "+")
@0: Anne is not smart.[(triple1)] Bob is nice.[(triple2)] Charlie is furry.[(triple3)] Erin is nice.[(triple4)] @1: Bob is cold.[(((triple2) -> rule2))] Bob is furry.[(((triple2) -> rule4))] Bob is white.[(((triple2) -> rule6))] Charlie is not smart.[(((triple3) -> rule1))] Erin is cold.[(((triple4) -> rule2))] Erin is furry.[(((triple4) -> rule4))] Erin is white.[(((triple4) -> rule6))] @2: Bob is not smart.[(((((triple2) -> rule4)) -> rule1))] Erin is not smart.[(((((triple4) -> rule4)) -> rule1))]
Anne is not smart.
("Anne" "is" "smart" "-")
triple1
Bob is nice.
("Bob" "is" "nice" "+")
triple2
Charlie is furry.
("Charlie" "is" "furry" "+")
triple3
Erin is nice.
("Erin" "is" "nice" "+")
triple4
Bob is cold.
("Bob" "is" "cold" "+")
((triple2) -> (rule2 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
((triple2) -> (rule4 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
((triple2) -> (rule6 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Charlie is not smart.
("Charlie" "is" "smart" "-")
((triple3) -> (rule1 % int1))
Charlie is not smart.
("Charlie" "is" "smart" "-")
int1
Erin is cold.
("Erin" "is" "cold" "+")
((triple4) -> (rule2 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
((triple4) -> (rule4 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
((triple4) -> (rule6 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Bob is not smart.
("Bob" "is" "smart" "-")
((((triple2) -> (rule4 % int2))) -> (rule1 % int1))
Bob is not smart.
("Bob" "is" "smart" "-")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Erin is not smart.
("Erin" "is" "smart" "-")
((((triple4) -> (rule4 % int2))) -> (rule1 % int1))
Erin is not smart.
("Erin" "is" "smart" "-")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2