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