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