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