Bob is blue. Dave is white. Fiona is white. If someone is red then they are cold. If someone is blue then they are cold. If someone is green and rough then they are white. All cold people are furry. Rough people are furry. If someone is blue then they are not green. If Fiona is red then Fiona is furry. White, blue people are red.
Bob is blue.
("Bob" "is" "blue" "+")
Dave is white.
("Dave" "is" "white" "+")
Fiona is white.
("Fiona" "is" "white" "+")
If someone is red then they are cold.
((("someone" "is" "red" "+")) -> ("someone" "is" "cold" "+"))
If someone is blue then they are cold.
((("someone" "is" "blue" "+")) -> ("someone" "is" "cold" "+"))
If someone is green and rough then they are white.
((("someone" "is" "green" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "white" "+"))
All cold people are furry.
((("someone" "is" "cold" "+")) -> ("someone" "is" "furry" "+"))
Rough people are furry.
((("someone" "is" "rough" "+")) -> ("someone" "is" "furry" "+"))
If someone is blue then they are not green.
((("someone" "is" "blue" "+")) -> ("someone" "is" "green" "-"))
If Fiona is red then Fiona is furry.
((("Fiona" "is" "red" "+")) -> ("Fiona" "is" "furry" "+"))
White, blue people are red.
((("someone" "is" "white" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "red" "+"))
Bob is blue.
True
1
proof
[(triple1)]
("Bob" "is" "blue" "+")
triple1
Bob is not blue.
False
1
inv-proof
[(triple1)]
("Bob" "is" "blue" "-")
triple1
Bob is not green.
True
2
proof
[(((triple1) -> rule6))]
("Bob" "is" "green" "-")
((triple1) -> (rule6 % int1))
Bob is not green.
("Bob" "is" "green" "-")
int1
Bob is green.
False
2
inv-proof
[(((triple1) -> rule6))]
("Bob" "is" "green" "+")
((triple1) -> (rule6 % int1))
Bob is not green.
("Bob" "is" "green" "-")
int1
Bob is furry.
True
3
proof
[(((((triple1) -> rule2)) -> rule4))]
("Bob" "is" "furry" "+")
((((triple1) -> (rule2 % int2))) -> (rule4 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is not furry.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule4))]
("Bob" "is" "furry" "-")
((((triple1) -> (rule2 % int2))) -> (rule4 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Fiona is not red.
Unknown
inv-rconc
[@1: Fiona is red.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Fiona" "is" "red" "-")
Fiona is furry.
Unknown
rconc
[@3: Fiona is furry.[CWA. Example of deepest failure = (rule4 <- rule1 <- rule8 <- FAIL)]]
("Fiona" "is" "furry" "+")
Dave is not red.
Unknown
inv-rconc
[@1: Dave is red.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Dave" "is" "red" "-")
Dave is rough.
Unknown
random
[@0: Dave is rough.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "rough" "+")
Fiona is not blue.
Unknown
inv-random
[@0: Fiona is blue.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "blue" "-")
Dave is blue.
Unknown
random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "+")
@0: Bob is blue.[(triple1)] Dave is white.[(triple2)] Fiona is white.[(triple3)] @1: Bob is cold.[(((triple1) -> rule2))] Bob is not green.[(((triple1) -> rule6))] @2: Bob is furry.[(((((triple1) -> rule2)) -> rule4))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Dave is white.
("Dave" "is" "white" "+")
triple2
Fiona is white.
("Fiona" "is" "white" "+")
triple3
Bob is cold.
("Bob" "is" "cold" "+")
((triple1) -> (rule2 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is not green.
("Bob" "is" "green" "-")
((triple1) -> (rule6 % int1))
Bob is not green.
("Bob" "is" "green" "-")
int1
Bob is furry.
("Bob" "is" "furry" "+")
((((triple1) -> (rule2 % int2))) -> (rule4 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2