Charlie is not green. Dave is quiet. Gary is green. If someone is rough and not blue then they are not white. Furry people are nice. All rough people are not green. All quiet, nice people are green. Quiet people are furry. If Charlie is quiet then Charlie is not nice.
Charlie is not green.
("Charlie" "is" "green" "-")
Dave is quiet.
("Dave" "is" "quiet" "+")
Gary is green.
("Gary" "is" "green" "+")
If someone is rough and not blue then they are not white.
((("someone" "is" "rough" "+") ("someone" "is" "blue" "~")) -> ("someone" "is" "white" "-"))
Furry people are nice.
((("someone" "is" "furry" "+")) -> ("someone" "is" "nice" "+"))
All rough people are not green.
((("someone" "is" "rough" "+")) -> ("someone" "is" "green" "-"))
All quiet, nice people are green.
((("someone" "is" "quiet" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "green" "+"))
Quiet people are furry.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "furry" "+"))
If Charlie is quiet then Charlie is not nice.
((("Charlie" "is" "quiet" "+")) -> ("Charlie" "is" "nice" "-"))
Dave is quiet.
True
1
proof
[(triple2)]
("Dave" "is" "quiet" "+")
triple2
Gary is not green.
False
1
inv-proof
[(triple3)]
("Gary" "is" "green" "-")
triple3
Dave is furry.
True
2
proof
[(((triple2) -> rule5))]
("Dave" "is" "furry" "+")
((triple2) -> (rule5 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is not furry.
False
2
inv-proof
[(((triple2) -> rule5))]
("Dave" "is" "furry" "-")
((triple2) -> (rule5 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is nice.
True
3
proof
[(((((triple2) -> rule5)) -> rule2))]
("Dave" "is" "nice" "+")
((((triple2) -> (rule5 % int2))) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is not nice.
False
3
inv-proof
[(((((triple2) -> rule5)) -> rule2))]
("Dave" "is" "nice" "-")
((((triple2) -> (rule5 % int2))) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is green.
True
5
proof
[(((triple2 ((((triple2) -> rule5)) -> rule2)) -> rule4))]
("Dave" "is" "green" "+")
((triple2 ((((triple2) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Dave is not green.
False
5
inv-proof
[(((triple2 ((((triple2) -> rule5)) -> rule2)) -> rule4))]
("Dave" "is" "green" "-")
((triple2 ((((triple2) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Charlie is not furry.
Unknown
inv-rconc
[@1: Charlie is furry.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Charlie" "is" "furry" "-")
Gary is furry.
Unknown
rconc
[@1: Gary is furry.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Gary" "is" "furry" "+")
Charlie is not nice.
Unknown
inv-rconc
[@2: Charlie is nice.[CWA. Example of deepest failure = (rule2 <- rule5 <- FAIL)]]
("Charlie" "is" "nice" "-")
Gary is nice.
Unknown
rconc
[@2: Gary is nice.[CWA. Example of deepest failure = (rule2 <- rule5 <- FAIL)]]
("Gary" "is" "nice" "+")
Gary is not quiet.
Unknown
inv-random
[@0: Gary is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "quiet" "-")
Dave is rough.
Unknown
random
[@0: Dave is rough.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "rough" "+")
Gary is not white.
Unknown
inv-random
[@0: Gary is white.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "white" "-")
Dave is blue.
Unknown
random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "+")
@0: Charlie is not green.[(triple1)] Dave is quiet.[(triple2)] Gary is green.[(triple3)] @1: Dave is furry.[(((triple2) -> rule5))] @2: Dave is nice.[(((((triple2) -> rule5)) -> rule2))] @3: Dave is green.[(((triple2 ((((triple2) -> rule5)) -> rule2)) -> rule4))]
Charlie is not green.
("Charlie" "is" "green" "-")
triple1
Dave is quiet.
("Dave" "is" "quiet" "+")
triple2
Gary is green.
("Gary" "is" "green" "+")
triple3
Dave is furry.
("Dave" "is" "furry" "+")
((triple2) -> (rule5 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
((((triple2) -> (rule5 % int2))) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
((triple2 ((((triple2) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3