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