Bob is not kind. Bob is nice. Dave is nice. Erin is cold. Gary is not cold. Gary is furry. Gary is kind. If something is furry and red then it is not white. If Erin is kind then Erin is white. If something is furry then it is red. Furry things are not young. If something is young then it is nice. If something is kind and not white then it is nice.
Bob is not kind.
("Bob" "is" "kind" "-")
Bob is nice.
("Bob" "is" "nice" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Gary is not cold.
("Gary" "is" "cold" "-")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is kind.
("Gary" "is" "kind" "+")
If something is furry and red then it is not white.
((("something" "is" "furry" "+") ("something" "is" "red" "+")) -> ("something" "is" "white" "-"))
If Erin is kind then Erin is white.
((("Erin" "is" "kind" "+")) -> ("Erin" "is" "white" "+"))
If something is furry then it is red.
((("something" "is" "furry" "+")) -> ("something" "is" "red" "+"))
Furry things are not young.
((("something" "is" "furry" "+")) -> ("something" "is" "young" "-"))
If something is young then it is nice.
((("something" "is" "young" "+")) -> ("something" "is" "nice" "+"))
If something is kind and not white then it is nice.
((("something" "is" "kind" "+") ("something" "is" "white" "~")) -> ("something" "is" "nice" "+"))
Erin is cold.
True
1
proof
[(triple4)]
("Erin" "is" "cold" "+")
triple4
Bob is kind.
False
1
inv-proof
[(triple1)]
("Bob" "is" "kind" "+")
triple1
Gary is not young.
True
2
proof
[(((triple6) -> rule4))]
("Gary" "is" "young" "-")
((triple6) -> (rule4 % int1))
Gary is not young.
("Gary" "is" "young" "-")
int1
Gary is young.
False
2
inv-proof
[(((triple6) -> rule4))]
("Gary" "is" "young" "+")
((triple6) -> (rule4 % int1))
Gary is not young.
("Gary" "is" "young" "-")
int1
Gary is not white.
True
4
proof
[(((triple6 ((triple6) -> rule3)) -> rule1))]
("Gary" "is" "white" "-")
((triple6 ((triple6) -> (rule3 % int2))) -> (rule1 % int1))
Gary is not white.
("Gary" "is" "white" "-")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is white.
False
4
inv-proof
[(((triple6 ((triple6) -> rule3)) -> rule1))]
("Gary" "is" "white" "+")
((triple6 ((triple6) -> (rule3 % int2))) -> (rule1 % int1))
Gary is not white.
("Gary" "is" "white" "-")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is nice.
True
6
proof
[(((triple7 ((triple6 ((triple6) -> rule3)) -> rule1)) -> rule6))]
("Gary" "is" "nice" "+")
((triple7 ((triple6 ((triple6) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is not white.
("Gary" "is" "white" "-")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
Gary is not nice.
False
6
inv-proof
[(((triple7 ((triple6 ((triple6) -> rule3)) -> rule1)) -> rule6))]
("Gary" "is" "nice" "-")
((triple7 ((triple6 ((triple6) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is not white.
("Gary" "is" "white" "-")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
Erin is not red.
Unknown
inv-rconc
[@1: Erin is red.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Erin" "is" "red" "-")
Erin is white.
Unknown
rconc
[@1: Erin is white.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Erin" "is" "white" "+")
Erin is not nice.
Unknown
inv-rconc
[@1: Erin is nice.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Erin" "is" "nice" "-")
Dave is red.
Unknown
rconc
[@1: Dave is red.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "red" "+")
Bob is not cold.
Unknown
inv-random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "-")
Bob is young.
Unknown
random
[@0: Bob is young.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "young" "+")
Erin is not furry.
Unknown
inv-random
[@0: Erin is furry.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "furry" "-")
Bob is white.
Unknown
random
[@0: Bob is white.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "white" "+")
@0: Bob is nice.[(triple2)] Bob is not kind.[(triple1)] Dave is nice.[(triple3)] Erin is cold.[(triple4)] Gary is furry.[(triple6)] Gary is kind.[(triple7)] Gary is not cold.[(triple5)] @1: Gary is not young.[(((triple6) -> rule4))] Gary is red.[(((triple6) -> rule3))] @2: Gary is not white.[(((triple6 ((triple6) -> rule3)) -> rule1))] @3: Gary is nice.[(((triple7 ((triple6 ((triple6) -> rule3)) -> rule1)) -> rule6))]
Bob is nice.
("Bob" "is" "nice" "+")
triple2
Bob is not kind.
("Bob" "is" "kind" "-")
triple1
Dave is nice.
("Dave" "is" "nice" "+")
triple3
Erin is cold.
("Erin" "is" "cold" "+")
triple4
Gary is furry.
("Gary" "is" "furry" "+")
triple6
Gary is kind.
("Gary" "is" "kind" "+")
triple7
Gary is not cold.
("Gary" "is" "cold" "-")
triple5
Gary is not young.
("Gary" "is" "young" "-")
((triple6) -> (rule4 % int1))
Gary is not young.
("Gary" "is" "young" "-")
int1
Gary is red.
("Gary" "is" "red" "+")
((triple6) -> (rule3 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is not white.
("Gary" "is" "white" "-")
((triple6 ((triple6) -> (rule3 % int2))) -> (rule1 % int1))
Gary is not white.
("Gary" "is" "white" "-")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
((triple7 ((triple6 ((triple6) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is not white.
("Gary" "is" "white" "-")
int2
Gary is red.
("Gary" "is" "red" "+")
int3