Erin is quiet. Gary is furry. If Erin is quiet and Erin is kind then Erin is cold. Quiet people are kind. If Erin is cold and Erin is kind then Erin is nice.
Erin is quiet.
("Erin" "is" "quiet" "+")
Gary is furry.
("Gary" "is" "furry" "+")
If Erin is quiet and Erin is kind then Erin is cold.
((("Erin" "is" "quiet" "+") ("Erin" "is" "kind" "+")) -> ("Erin" "is" "cold" "+"))
Quiet people are kind.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "kind" "+"))
If Erin is cold and Erin is kind then Erin is nice.
((("Erin" "is" "cold" "+") ("Erin" "is" "kind" "+")) -> ("Erin" "is" "nice" "+"))
Erin is quiet.
True
1
proof
[(triple1)]
("Erin" "is" "quiet" "+")
triple1
Erin is not quiet.
False
1
inv-proof
[(triple1)]
("Erin" "is" "quiet" "-")
triple1
Erin is kind.
True
2
proof
[(((triple1) -> rule2))]
("Erin" "is" "kind" "+")
((triple1) -> (rule2 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is not kind.
False
2
inv-proof
[(((triple1) -> rule2))]
("Erin" "is" "kind" "-")
((triple1) -> (rule2 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is cold.
True
4
proof
[(((triple1 ((triple1) -> rule2)) -> rule1))]
("Erin" "is" "cold" "+")
((triple1 ((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is not cold.
False
4
inv-proof
[(((triple1 ((triple1) -> rule2)) -> rule1))]
("Erin" "is" "cold" "-")
((triple1 ((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is nice.
True
7
proof
[(((((triple1 ((triple1) -> rule2)) -> rule1) ((triple1) -> rule2)) -> rule3))]
("Erin" "is" "nice" "+")
((((triple1 ((triple1) -> (rule2 % int3))) -> (rule1 % int2)) ((triple1) -> (rule2 % int3))) -> (rule3 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Erin is not nice.
False
7
inv-proof
[(((((triple1 ((triple1) -> rule2)) -> rule1) ((triple1) -> rule2)) -> rule3))]
("Erin" "is" "nice" "-")
((((triple1 ((triple1) -> (rule2 % int3))) -> (rule1 % int2)) ((triple1) -> (rule2 % int3))) -> (rule3 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Gary is not kind.
Unknown
inv-rconc
[@1: Gary is kind.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "kind" "-")
Erin is smart.
Unknown
random
[@0: Erin is smart.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "smart" "+")
Gary is not nice.
Unknown
inv-random
[@0: Gary is nice.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "nice" "-")
Gary is smart.
Unknown
random
[@0: Gary is smart.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "smart" "+")
Erin is not furry.
Unknown
inv-random
[@0: Erin is furry.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "furry" "-")
Gary is quiet.
Unknown
random
[@0: Gary is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "quiet" "+")
Gary is not cold.
Unknown
inv-random
[@0: Gary is cold.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "cold" "-")
Gary is young.
Unknown
random
[@0: Gary is young.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "young" "+")
@0: Erin is quiet.[(triple1)] Gary is furry.[(triple2)] @1: Erin is kind.[(((triple1) -> rule2))] @2: Erin is cold.[(((triple1 ((triple1) -> rule2)) -> rule1))] @3: Erin is nice.[(((((triple1 ((triple1) -> rule2)) -> rule1) ((triple1) -> rule2)) -> rule3))]
Erin is quiet.
("Erin" "is" "quiet" "+")
triple1
Gary is furry.
("Gary" "is" "furry" "+")
triple2
Erin is kind.
("Erin" "is" "kind" "+")
((triple1) -> (rule2 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
((triple1 ((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
((((triple1 ((triple1) -> (rule2 % int3))) -> (rule1 % int2)) ((triple1) -> (rule2 % int3))) -> (rule3 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3