Bob is furry. Erin is kind. Fiona is kind. Gary is rough. Cold people are blue. All smart, kind people are furry. Blue, cold people are kind. All cold people are blue. If Gary is kind then Gary is blue. If someone is rough then they are cold.
Bob is furry.
("Bob" "is" "furry" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Cold people are blue.
((("someone" "is" "cold" "+")) -> ("someone" "is" "blue" "+"))
All smart, kind people are furry.
((("someone" "is" "smart" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "furry" "+"))
Blue, cold people are kind.
((("someone" "is" "blue" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "kind" "+"))
All cold people are blue.
((("someone" "is" "cold" "+")) -> ("someone" "is" "blue" "+"))
If Gary is kind then Gary is blue.
((("Gary" "is" "kind" "+")) -> ("Gary" "is" "blue" "+"))
If someone is rough then they are cold.
((("someone" "is" "rough" "+")) -> ("someone" "is" "cold" "+"))
Fiona is kind.
True
1
proof
[(triple3)]
("Fiona" "is" "kind" "+")
triple3
Bob is not furry.
False
1
inv-proof
[(triple1)]
("Bob" "is" "furry" "-")
triple1
Gary is cold.
True
2
proof
[(((triple4) -> rule6))]
("Gary" "is" "cold" "+")
((triple4) -> (rule6 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is not cold.
False
2
inv-proof
[(((triple4) -> rule6))]
("Gary" "is" "cold" "-")
((triple4) -> (rule6 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is blue.
True
3
proof
[(((((triple4) -> rule6)) -> rule1) OR ((((triple4) -> rule6)) -> rule4))]
("Gary" "is" "blue" "+")
((((triple4) -> (rule6 % int2))) -> (rule1 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
((((triple4) -> (rule6 % int2))) -> (rule4 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is not blue.
False
3
inv-proof
[(((((triple4) -> rule6)) -> rule1) OR ((((triple4) -> rule6)) -> rule4))]
("Gary" "is" "blue" "-")
((((triple4) -> (rule6 % int2))) -> (rule1 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
((((triple4) -> (rule6 % int2))) -> (rule4 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Fiona is not blue.
Unknown
inv-rconc
[@2: Fiona is blue.[CWA. Example of deepest failure = (rule1 <- rule6 <- FAIL)]]
("Fiona" "is" "blue" "-")
Erin is blue.
Unknown
rconc
[@2: Erin is blue.[CWA. Example of deepest failure = (rule1 <- rule6 <- FAIL)]]
("Erin" "is" "blue" "+")
Bob is not blue.
Unknown
inv-rconc
[@2: Bob is blue.[CWA. Example of deepest failure = (rule1 <- rule6 <- FAIL)]]
("Bob" "is" "blue" "-")
Bob is rough.
Unknown
random
[@0: Bob is rough.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "rough" "+")
Erin is not red.
Unknown
inv-random
[@0: Erin is red.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "red" "-")
Fiona is smart.
Unknown
random
[@0: Fiona is smart.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "smart" "+")
@0: Bob is furry.[(triple1)] Erin is kind.[(triple2)] Fiona is kind.[(triple3)] Gary is rough.[(triple4)] @1: Gary is cold.[(((triple4) -> rule6))] @2: Gary is blue.[(((((triple4) -> rule6)) -> rule1) OR ((((triple4) -> rule6)) -> rule4))] @3: Gary is kind.[(((((((triple4) -> rule6)) -> rule1) ((triple4) -> rule6)) -> rule3) OR ((((((triple4) -> rule6)) -> rule4) ((triple4) -> rule6)) -> rule3))]
Bob is furry.
("Bob" "is" "furry" "+")
triple1
Erin is kind.
("Erin" "is" "kind" "+")
triple2
Fiona is kind.
("Fiona" "is" "kind" "+")
triple3
Gary is rough.
("Gary" "is" "rough" "+")
triple4
Gary is cold.
("Gary" "is" "cold" "+")
((triple4) -> (rule6 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
((((triple4) -> (rule6 % int2))) -> (rule1 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
((((triple4) -> (rule6 % int2))) -> (rule4 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
((((((triple4) -> (rule6 % int3))) -> (rule1 % int2)) ((triple4) -> (rule6 % int3))) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
((((((triple4) -> (rule6 % int3))) -> (rule4 % int2)) ((triple4) -> (rule6 % int3))) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3