Charlie is not kind. Erin is quiet. Gary is furry. Harry is cold. Quiet things are furry. If something is furry then it is kind. Kind things are rough. If Charlie is red then Charlie is not rough. All furry things are quiet. All furry, rough things are cold.
Charlie is not kind.
("Charlie" "is" "kind" "-")
Erin is quiet.
("Erin" "is" "quiet" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Quiet things are furry.
((("something" "is" "quiet" "+")) -> ("something" "is" "furry" "+"))
If something is furry then it is kind.
((("something" "is" "furry" "+")) -> ("something" "is" "kind" "+"))
Kind things are rough.
((("something" "is" "kind" "+")) -> ("something" "is" "rough" "+"))
If Charlie is red then Charlie is not rough.
((("Charlie" "is" "red" "+")) -> ("Charlie" "is" "rough" "-"))
All furry things are quiet.
((("something" "is" "furry" "+")) -> ("something" "is" "quiet" "+"))
All furry, rough things are cold.
((("something" "is" "furry" "+") ("something" "is" "rough" "+")) -> ("something" "is" "cold" "+"))
Gary is furry.
True
1
proof
[(triple3)]
("Gary" "is" "furry" "+")
triple3
Charlie is kind.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "kind" "+")
triple1
Erin is furry.
True
2
proof
[(((triple2) -> rule1))]
("Erin" "is" "furry" "+")
((triple2) -> (rule1 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is not furry.
False
2
inv-proof
[(((triple2) -> rule1))]
("Erin" "is" "furry" "-")
((triple2) -> (rule1 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is kind.
True
3
proof
[(((((triple2) -> rule1)) -> rule2))]
("Erin" "is" "kind" "+")
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Gary is not rough.
False
3
inv-proof
[(((((triple3) -> rule2)) -> rule3))]
("Gary" "is" "rough" "-")
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is cold.
True
5
proof
[(((triple3 ((((triple3) -> rule2)) -> rule3)) -> rule6))]
("Gary" "is" "cold" "+")
((triple3 ((((triple3) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3
Gary is not cold.
False
5
inv-proof
[(((triple3 ((((triple3) -> rule2)) -> rule3)) -> rule6))]
("Gary" "is" "cold" "-")
((triple3 ((((triple3) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3
Charlie is not furry.
Unknown
inv-rconc
[@2: Charlie is furry.[CWA. Example of deepest failure = (rule1 <- rule5 <- FAIL)]]
("Charlie" "is" "furry" "-")
Charlie is quiet.
Unknown
rconc
[@2: Charlie is quiet.[CWA. Example of deepest failure = (rule5 <- rule1 <- FAIL)]]
("Charlie" "is" "quiet" "+")
Harry is not kind.
Unknown
inv-rconc
[@3: Harry is kind.[CWA. Example of deepest failure = (rule2 <- rule1 <- rule5 <- FAIL)]]
("Harry" "is" "kind" "-")
Harry is furry.
Unknown
rconc
[@2: Harry is furry.[CWA. Example of deepest failure = (rule1 <- rule5 <- FAIL)]]
("Harry" "is" "furry" "+")
Gary is not red.
Unknown
inv-random
[@0: Gary is red.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "red" "-")
Harry is red.
Unknown
random
[@0: Harry is red.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "red" "+")
Erin is not red.
Unknown
inv-random
[@0: Erin is red.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "red" "-")
Harry is nice.
Unknown
random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "+")
@0: Charlie is not kind.[(triple1)] Erin is quiet.[(triple2)] Gary is furry.[(triple3)] Harry is cold.[(triple4)] @1: Erin is furry.[(((triple2) -> rule1))] Gary is kind.[(((triple3) -> rule2))] Gary is quiet.[(((triple3) -> rule5))] @2: Erin is kind.[(((((triple2) -> rule1)) -> rule2))] Gary is rough.[(((((triple3) -> rule2)) -> rule3))] @3: Erin is rough.[(((((((triple2) -> rule1)) -> rule2)) -> rule3))] Gary is cold.[(((triple3 ((((triple3) -> rule2)) -> rule3)) -> rule6))] @4: Erin is cold.[(((((triple2) -> rule1) ((((((triple2) -> rule1)) -> rule2)) -> rule3)) -> rule6))]
Charlie is not kind.
("Charlie" "is" "kind" "-")
triple1
Erin is quiet.
("Erin" "is" "quiet" "+")
triple2
Gary is furry.
("Gary" "is" "furry" "+")
triple3
Harry is cold.
("Harry" "is" "cold" "+")
triple4
Erin is furry.
("Erin" "is" "furry" "+")
((triple2) -> (rule1 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
((triple3) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
((triple3) -> (rule5 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
((((((triple2) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3
Gary is cold.
("Gary" "is" "cold" "+")
((triple3 ((((triple3) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3
Erin is cold.
("Erin" "is" "cold" "+")
((((triple2) -> (rule1 % int4)) ((((((triple2) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Erin is furry.
("Erin" "is" "furry" "+")
int4