Dave is nice. Erin is green. Fiona is rough. Gary is kind. All kind, quiet people are rough. All kind people are furry. If someone is green then they are not nice. If Gary is rough then Gary is not nice. If someone is furry then they are green. If someone is green then they are quiet.
Dave is nice.
("Dave" "is" "nice" "+")
Erin is green.
("Erin" "is" "green" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Gary is kind.
("Gary" "is" "kind" "+")
All kind, quiet people are rough.
((("someone" "is" "kind" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "rough" "+"))
All kind people are furry.
((("someone" "is" "kind" "+")) -> ("someone" "is" "furry" "+"))
If someone is green then they are not nice.
((("someone" "is" "green" "+")) -> ("someone" "is" "nice" "-"))
If Gary is rough then Gary is not nice.
((("Gary" "is" "rough" "+")) -> ("Gary" "is" "nice" "-"))
If someone is furry then they are green.
((("someone" "is" "furry" "+")) -> ("someone" "is" "green" "+"))
If someone is green then they are quiet.
((("someone" "is" "green" "+")) -> ("someone" "is" "quiet" "+"))
Gary is kind.
True
1
proof
[(triple4)]
("Gary" "is" "kind" "+")
triple4
Erin is not green.
False
1
inv-proof
[(triple2)]
("Erin" "is" "green" "-")
triple2
Erin is not nice.
True
2
proof
[(((triple2) -> rule3))]
("Erin" "is" "nice" "-")
((triple2) -> (rule3 % int1))
Erin is not nice.
("Erin" "is" "nice" "-")
int1
Erin is not quiet.
False
2
inv-proof
[(((triple2) -> rule6))]
("Erin" "is" "quiet" "-")
((triple2) -> (rule6 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Gary is green.
True
3
proof
[(((((triple4) -> rule2)) -> rule5))]
("Gary" "is" "green" "+")
((((triple4) -> (rule2 % int2))) -> (rule5 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is not green.
False
3
inv-proof
[(((((triple4) -> rule2)) -> rule5))]
("Gary" "is" "green" "-")
((((triple4) -> (rule2 % int2))) -> (rule5 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is quiet.
True
4
proof
[(((((((triple4) -> rule2)) -> rule5)) -> rule6))]
("Gary" "is" "quiet" "+")
((((((triple4) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3
Gary is nice.
False
4
inv-proof
[(((((((triple4) -> rule2)) -> rule5)) -> rule3) OR ((((triple4 ((((((triple4) -> rule2)) -> rule5)) -> rule6)) -> rule1)) -> rule4))]
("Gary" "is" "nice" "+")
((((((triple4) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Gary is not nice.
("Gary" "is" "nice" "-")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3
((((triple4 ((((((triple4) -> (rule2 % int5))) -> (rule5 % int4))) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Gary is not nice.
("Gary" "is" "nice" "-")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Gary is green.
("Gary" "is" "green" "+")
int4
Gary is furry.
("Gary" "is" "furry" "+")
int5
Fiona is not furry.
Unknown
inv-rconc
[@1: Fiona is furry.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Fiona" "is" "furry" "-")
Dave is green.
Unknown
rconc
[@2: Dave is green.[CWA. Example of deepest failure = (rule5 <- rule2 <- FAIL)]]
("Dave" "is" "green" "+")
Dave is not furry.
Unknown
inv-rconc
[@1: Dave is furry.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "furry" "-")
Fiona is quiet.
Unknown
rconc
[@3: Fiona is quiet.[CWA. Example of deepest failure = (rule6 <- rule5 <- rule2 <- FAIL)]]
("Fiona" "is" "quiet" "+")
Fiona is not kind.
Unknown
inv-random
[@0: Fiona is kind.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "kind" "-")
Erin is kind.
Unknown
random
[@0: Erin is kind.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "kind" "+")
Erin is not young.
Unknown
inv-random
[@0: Erin is young.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "young" "-")
Dave is young.
Unknown
random
[@0: Dave is young.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "young" "+")
@0: Dave is nice.[(triple1)] Erin is green.[(triple2)] Fiona is rough.[(triple3)] Gary is kind.[(triple4)] @1: Erin is not nice.[(((triple2) -> rule3))] Erin is quiet.[(((triple2) -> rule6))] Gary is furry.[(((triple4) -> rule2))] @2: Gary is green.[(((((triple4) -> rule2)) -> rule5))] @3: Gary is not nice.[(((((((triple4) -> rule2)) -> rule5)) -> rule3) OR ((((triple4 ((((((triple4) -> rule2)) -> rule5)) -> rule6)) -> rule1)) -> rule4))] Gary is quiet.[(((((((triple4) -> rule2)) -> rule5)) -> rule6))] @4: Gary is rough.[(((triple4 ((((((triple4) -> rule2)) -> rule5)) -> rule6)) -> rule1))]
Dave is nice.
("Dave" "is" "nice" "+")
triple1
Erin is green.
("Erin" "is" "green" "+")
triple2
Fiona is rough.
("Fiona" "is" "rough" "+")
triple3
Gary is kind.
("Gary" "is" "kind" "+")
triple4
Erin is not nice.
("Erin" "is" "nice" "-")
((triple2) -> (rule3 % int1))
Erin is not nice.
("Erin" "is" "nice" "-")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
((triple2) -> (rule6 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
((triple4) -> (rule2 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
((((triple4) -> (rule2 % int2))) -> (rule5 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is not nice.
("Gary" "is" "nice" "-")
((((((triple4) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Gary is not nice.
("Gary" "is" "nice" "-")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3
((((triple4 ((((((triple4) -> (rule2 % int5))) -> (rule5 % int4))) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Gary is not nice.
("Gary" "is" "nice" "-")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Gary is green.
("Gary" "is" "green" "+")
int4
Gary is furry.
("Gary" "is" "furry" "+")
int5
Gary is quiet.
("Gary" "is" "quiet" "+")
((((((triple4) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3
Gary is rough.
("Gary" "is" "rough" "+")
((triple4 ((((((triple4) -> (rule2 % int4))) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
Gary is furry.
("Gary" "is" "furry" "+")
int4