Bob is kind. Erin is red. Fiona is big. Big, furry people are white. If someone is big and white then they are blue. All furry people are blue. All blue people are kind. If someone is white and not rough then they are not kind. Red people are furry.
Bob is kind.
("Bob" "is" "kind" "+")
Erin is red.
("Erin" "is" "red" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Big, furry people are white.
((("someone" "is" "big" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "white" "+"))
If someone is big and white then they are blue.
((("someone" "is" "big" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "blue" "+"))
All furry people are blue.
((("someone" "is" "furry" "+")) -> ("someone" "is" "blue" "+"))
All blue people are kind.
((("someone" "is" "blue" "+")) -> ("someone" "is" "kind" "+"))
If someone is white and not rough then they are not kind.
((("someone" "is" "white" "+") ("someone" "is" "rough" "~")) -> ("someone" "is" "kind" "-"))
Red people are furry.
((("someone" "is" "red" "+")) -> ("someone" "is" "furry" "+"))
Bob is kind.
True
1
proof
[(triple1)]
("Bob" "is" "kind" "+")
triple1
Bob is not kind.
False
1
inv-proof
[(triple1)]
("Bob" "is" "kind" "-")
triple1
Erin is furry.
True
2
proof
[(((triple2) -> rule6))]
("Erin" "is" "furry" "+")
((triple2) -> (rule6 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is not furry.
False
2
inv-proof
[(((triple2) -> rule6))]
("Erin" "is" "furry" "-")
((triple2) -> (rule6 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is blue.
True
3
proof
[(((((triple2) -> rule6)) -> rule3))]
("Erin" "is" "blue" "+")
((((triple2) -> (rule6 % int2))) -> (rule3 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is not blue.
False
3
inv-proof
[(((((triple2) -> rule6)) -> rule3))]
("Erin" "is" "blue" "-")
((((triple2) -> (rule6 % int2))) -> (rule3 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is kind.
True
4
proof
[(((((((triple2) -> rule6)) -> rule3)) -> rule4))]
("Erin" "is" "kind" "+")
((((((triple2) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3
Erin is not kind.
False
4
inv-proof
[(((((((triple2) -> rule6)) -> rule3)) -> rule4))]
("Erin" "is" "kind" "-")
((((((triple2) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3
Erin is not white.
Unknown
inv-rconc
[@1: Erin is white.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "white" "-")
Fiona is kind.
Unknown
rconc
[@4: Fiona is kind.[CWA. Example of deepest failure = (rule4 <- rule2 <- rule1 <- rule6 <- FAIL)]]
("Fiona" "is" "kind" "+")
Bob is not furry.
Unknown
inv-rconc
[@1: Bob is furry.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Bob" "is" "furry" "-")
Fiona is blue.
Unknown
rconc
[@3: Fiona is blue.[CWA. Example of deepest failure = (rule2 <- rule1 <- rule6 <- FAIL)]]
("Fiona" "is" "blue" "+")
Bob is not red.
Unknown
inv-random
[@0: Bob is red.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "red" "-")
Fiona is rough.
Unknown
random
[@0: Fiona is rough.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "rough" "+")
Bob is not big.
Unknown
inv-random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "-")
Erin is big.
Unknown
random
[@0: Erin is big.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "big" "+")
@0: Bob is kind.[(triple1)] Erin is red.[(triple2)] Fiona is big.[(triple3)] @1: Erin is furry.[(((triple2) -> rule6))] @2: Erin is blue.[(((((triple2) -> rule6)) -> rule3))] @3: Erin is kind.[(((((((triple2) -> rule6)) -> rule3)) -> rule4))]
Bob is kind.
("Bob" "is" "kind" "+")
triple1
Erin is red.
("Erin" "is" "red" "+")
triple2
Fiona is big.
("Fiona" "is" "big" "+")
triple3
Erin is furry.
("Erin" "is" "furry" "+")
((triple2) -> (rule6 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
((((triple2) -> (rule6 % int2))) -> (rule3 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
((((((triple2) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3