Bob is quiet. Bob is round. Erin is furry. All rough, quiet people are cold. If someone is rough then they are cold. Red people are quiet. If someone is kind then they are quiet. Furry people are kind. Furry people are not red.
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is round.
("Bob" "is" "round" "+")
Erin is furry.
("Erin" "is" "furry" "+")
All rough, quiet people are cold.
((("someone" "is" "rough" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "cold" "+"))
If someone is rough then they are cold.
((("someone" "is" "rough" "+")) -> ("someone" "is" "cold" "+"))
Red people are quiet.
((("someone" "is" "red" "+")) -> ("someone" "is" "quiet" "+"))
If someone is kind then they are quiet.
((("someone" "is" "kind" "+")) -> ("someone" "is" "quiet" "+"))
Furry people are kind.
((("someone" "is" "furry" "+")) -> ("someone" "is" "kind" "+"))
Furry people are not red.
((("someone" "is" "furry" "+")) -> ("someone" "is" "red" "-"))
Bob is quiet.
True
1
proof
[(triple1)]
("Bob" "is" "quiet" "+")
triple1
Erin is not furry.
False
1
inv-proof
[(triple3)]
("Erin" "is" "furry" "-")
triple3
Erin is not red.
True
2
proof
[(((triple3) -> rule6))]
("Erin" "is" "red" "-")
((triple3) -> (rule6 % int1))
Erin is not red.
("Erin" "is" "red" "-")
int1
Erin is red.
False
2
inv-proof
[(((triple3) -> rule6))]
("Erin" "is" "red" "+")
((triple3) -> (rule6 % int1))
Erin is not red.
("Erin" "is" "red" "-")
int1
Erin is quiet.
True
3
proof
[(((((triple3) -> rule5)) -> rule4))]
("Erin" "is" "quiet" "+")
((((triple3) -> (rule5 % int2))) -> (rule4 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is not quiet.
False
3
inv-proof
[(((((triple3) -> rule5)) -> rule4))]
("Erin" "is" "quiet" "-")
((((triple3) -> (rule5 % int2))) -> (rule4 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Bob is not kind.
Unknown
inv-rconc
[@1: Bob is kind.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Bob" "is" "kind" "-")
Erin is cold.
Unknown
rconc
[@1: Erin is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "cold" "+")
Bob is not cold.
Unknown
inv-rconc
[@1: Bob is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "cold" "-")
Bob is furry.
Unknown
random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "+")
Erin is not rough.
Unknown
inv-random
[@0: Erin is rough.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "rough" "-")
Erin is round.
Unknown
random
[@0: Erin is round.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "round" "+")
@0: Bob is quiet.[(triple1)] Bob is round.[(triple2)] Erin is furry.[(triple3)] @1: Erin is kind.[(((triple3) -> rule5))] Erin is not red.[(((triple3) -> rule6))] @2: Erin is quiet.[(((((triple3) -> rule5)) -> rule4))]
Bob is quiet.
("Bob" "is" "quiet" "+")
triple1
Bob is round.
("Bob" "is" "round" "+")
triple2
Erin is furry.
("Erin" "is" "furry" "+")
triple3
Erin is kind.
("Erin" "is" "kind" "+")
((triple3) -> (rule5 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is not red.
("Erin" "is" "red" "-")
((triple3) -> (rule6 % int1))
Erin is not red.
("Erin" "is" "red" "-")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
((((triple3) -> (rule5 % int2))) -> (rule4 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2