Dave is rough. Fiona is not rough. Gary is nice. Nice people are green. If someone is green then they are furry. If someone is furry then they are white. If Dave is green and Dave is round then Dave is rough. If someone is round and not white then they are rough. Nice, green people are rough.
Dave is rough.
("Dave" "is" "rough" "+")
Fiona is not rough.
("Fiona" "is" "rough" "-")
Gary is nice.
("Gary" "is" "nice" "+")
Nice people are green.
((("someone" "is" "nice" "+")) -> ("someone" "is" "green" "+"))
If someone is green then they are furry.
((("someone" "is" "green" "+")) -> ("someone" "is" "furry" "+"))
If someone is furry then they are white.
((("someone" "is" "furry" "+")) -> ("someone" "is" "white" "+"))
If Dave is green and Dave is round then Dave is rough.
((("Dave" "is" "green" "+") ("Dave" "is" "round" "+")) -> ("Dave" "is" "rough" "+"))
If someone is round and not white then they are rough.
((("someone" "is" "round" "+") ("someone" "is" "white" "~")) -> ("someone" "is" "rough" "+"))
Nice, green people are rough.
((("someone" "is" "nice" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "rough" "+"))
Gary is nice.
True
1
proof
[(triple3)]
("Gary" "is" "nice" "+")
triple3
Gary is not nice.
False
1
inv-proof
[(triple3)]
("Gary" "is" "nice" "-")
triple3
Gary is green.
True
2
proof
[(((triple3) -> rule1))]
("Gary" "is" "green" "+")
((triple3) -> (rule1 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is not green.
False
2
inv-proof
[(((triple3) -> rule1))]
("Gary" "is" "green" "-")
((triple3) -> (rule1 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is rough.
True
4
proof
[(((triple3 ((triple3) -> rule1)) -> rule6))]
("Gary" "is" "rough" "+")
((triple3 ((triple3) -> (rule1 % int2))) -> (rule6 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is not furry.
False
3
inv-proof
[(((((triple3) -> rule1)) -> rule2))]
("Gary" "is" "furry" "-")
((((triple3) -> (rule1 % int2))) -> (rule2 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is white.
True
4
proof
[(((((((triple3) -> rule1)) -> rule2)) -> rule3))]
("Gary" "is" "white" "+")
((((((triple3) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
Gary is not white.
False
4
inv-proof
[(((((((triple3) -> rule1)) -> rule2)) -> rule3))]
("Gary" "is" "white" "-")
((((((triple3) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
Dave is not green.
Unknown
inv-rconc
[@1: Dave is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "green" "-")
Fiona is furry.
Unknown
rconc
[@2: Fiona is furry.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("Fiona" "is" "furry" "+")
Fiona is not white.
Unknown
inv-rconc
[@3: Fiona is white.[CWA. Example of deepest failure = (rule3 <- rule2 <- rule1 <- FAIL)]]
("Fiona" "is" "white" "-")
Dave is furry.
Unknown
rconc
[@2: Dave is furry.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("Dave" "is" "furry" "+")
Fiona is not nice.
Unknown
inv-random
[@0: Fiona is nice.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "nice" "-")
Fiona is quiet.
Unknown
random
[@0: Fiona is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "quiet" "+")
Dave is not quiet.
Unknown
inv-random
[@0: Dave is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "quiet" "-")
Gary is quiet.
Unknown
random
[@0: Gary is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "quiet" "+")
@0: Dave is rough.[(triple1)] Fiona is not rough.[(triple2)] Gary is nice.[(triple3)] @1: Gary is green.[(((triple3) -> rule1))] @2: Gary is furry.[(((((triple3) -> rule1)) -> rule2))] Gary is rough.[(((triple3 ((triple3) -> rule1)) -> rule6))] @3: Gary is white.[(((((((triple3) -> rule1)) -> rule2)) -> rule3))]
Dave is rough.
("Dave" "is" "rough" "+")
triple1
Fiona is not rough.
("Fiona" "is" "rough" "-")
triple2
Gary is nice.
("Gary" "is" "nice" "+")
triple3
Gary is green.
("Gary" "is" "green" "+")
((triple3) -> (rule1 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
((((triple3) -> (rule1 % int2))) -> (rule2 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
((triple3 ((triple3) -> (rule1 % int2))) -> (rule6 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
((((((triple3) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3