Erin is smart. Gary is cold. Gary is kind. White, kind things are nice. If something is kind then it is white. Kind, nice things are furry.
Erin is smart.
("Erin" "is" "smart" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is kind.
("Gary" "is" "kind" "+")
White, kind things are nice.
((("something" "is" "white" "+") ("something" "is" "kind" "+")) -> ("something" "is" "nice" "+"))
If something is kind then it is white.
((("something" "is" "kind" "+")) -> ("something" "is" "white" "+"))
Kind, nice things are furry.
((("something" "is" "kind" "+") ("something" "is" "nice" "+")) -> ("something" "is" "furry" "+"))
Erin is smart.
True
1
proof
[(triple1)]
("Erin" "is" "smart" "+")
triple1
Gary is not cold.
False
1
inv-proof
[(triple2)]
("Gary" "is" "cold" "-")
triple2
Gary is white.
True
2
proof
[(((triple3) -> rule2))]
("Gary" "is" "white" "+")
((triple3) -> (rule2 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is not white.
False
2
inv-proof
[(((triple3) -> rule2))]
("Gary" "is" "white" "-")
((triple3) -> (rule2 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is nice.
True
4
proof
[(((((triple3) -> rule2) triple3) -> rule1))]
("Gary" "is" "nice" "+")
((((triple3) -> (rule2 % int2)) triple3) -> (rule1 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is not nice.
False
4
inv-proof
[(((((triple3) -> rule2) triple3) -> rule1))]
("Gary" "is" "nice" "-")
((((triple3) -> (rule2 % int2)) triple3) -> (rule1 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is furry.
True
6
proof
[(((triple3 ((((triple3) -> rule2) triple3) -> rule1)) -> rule3))]
("Gary" "is" "furry" "+")
((triple3 ((((triple3) -> (rule2 % int3)) triple3) -> (rule1 % int2))) -> (rule3 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Gary is not furry.
False
6
inv-proof
[(((triple3 ((((triple3) -> rule2) triple3) -> rule1)) -> rule3))]
("Gary" "is" "furry" "-")
((triple3 ((((triple3) -> (rule2 % int3)) triple3) -> (rule1 % int2))) -> (rule3 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Erin is not white.
Unknown
inv-rconc
[@1: Erin is white.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Erin" "is" "white" "-")
Erin is furry.
Unknown
rconc
[@1: Erin is furry.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Erin" "is" "furry" "+")
Erin is not nice.
Unknown
inv-rconc
[@1: Erin is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "nice" "-")
Erin is green.
Unknown
random
[@0: Erin is green.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "green" "+")
Gary is not green.
Unknown
inv-random
[@0: Gary is green.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "green" "-")
Erin is kind.
Unknown
random
[@0: Erin is kind.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "kind" "+")
Gary is not smart.
Unknown
inv-random
[@0: Gary is smart.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "smart" "-")
Erin is cold.
Unknown
random
[@0: Erin is cold.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "cold" "+")
@0: Erin is smart.[(triple1)] Gary is cold.[(triple2)] Gary is kind.[(triple3)] @1: Gary is white.[(((triple3) -> rule2))] @2: Gary is nice.[(((((triple3) -> rule2) triple3) -> rule1))] @3: Gary is furry.[(((triple3 ((((triple3) -> rule2) triple3) -> rule1)) -> rule3))]
Erin is smart.
("Erin" "is" "smart" "+")
triple1
Gary is cold.
("Gary" "is" "cold" "+")
triple2
Gary is kind.
("Gary" "is" "kind" "+")
triple3
Gary is white.
("Gary" "is" "white" "+")
((triple3) -> (rule2 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
((((triple3) -> (rule2 % int2)) triple3) -> (rule1 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
((triple3 ((((triple3) -> (rule2 % int3)) triple3) -> (rule1 % int2))) -> (rule3 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3