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