Dave is green. Erin is nice. Gary is white. Harry is kind. If Harry is quiet and Harry is green then Harry is furry. Round things are furry. All white things are furry. If something is round and nice then it is green. If Harry is green and Harry is round then Harry is white. All furry things are nice. If something is round then it is kind. Nice, white things are quiet.
Dave is green.
("Dave" "is" "green" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Gary is white.
("Gary" "is" "white" "+")
Harry is kind.
("Harry" "is" "kind" "+")
If Harry is quiet and Harry is green then Harry is furry.
((("Harry" "is" "quiet" "+") ("Harry" "is" "green" "+")) -> ("Harry" "is" "furry" "+"))
Round things are furry.
((("something" "is" "round" "+")) -> ("something" "is" "furry" "+"))
All white things are furry.
((("something" "is" "white" "+")) -> ("something" "is" "furry" "+"))
If something is round and nice then it is green.
((("something" "is" "round" "+") ("something" "is" "nice" "+")) -> ("something" "is" "green" "+"))
If Harry is green and Harry is round then Harry is white.
((("Harry" "is" "green" "+") ("Harry" "is" "round" "+")) -> ("Harry" "is" "white" "+"))
All furry things are nice.
((("something" "is" "furry" "+")) -> ("something" "is" "nice" "+"))
If something is round then it is kind.
((("something" "is" "round" "+")) -> ("something" "is" "kind" "+"))
Nice, white things are quiet.
((("something" "is" "nice" "+") ("something" "is" "white" "+")) -> ("something" "is" "quiet" "+"))
Dave is green.
True
1
proof
[(triple1)]
("Dave" "is" "green" "+")
triple1
Harry is not kind.
False
1
inv-proof
[(triple4)]
("Harry" "is" "kind" "-")
triple4
Gary is furry.
True
2
proof
[(((triple3) -> rule3))]
("Gary" "is" "furry" "+")
((triple3) -> (rule3 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is not furry.
False
2
inv-proof
[(((triple3) -> rule3))]
("Gary" "is" "furry" "-")
((triple3) -> (rule3 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is nice.
True
3
proof
[(((((triple3) -> rule3)) -> rule6))]
("Gary" "is" "nice" "+")
((((triple3) -> (rule3 % int2))) -> (rule6 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is not nice.
False
3
inv-proof
[(((((triple3) -> rule3)) -> rule6))]
("Gary" "is" "nice" "-")
((((triple3) -> (rule3 % int2))) -> (rule6 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is quiet.
True
5
proof
[(((((((triple3) -> rule3)) -> rule6) triple3) -> rule8))]
("Gary" "is" "quiet" "+")
((((((triple3) -> (rule3 % int3))) -> (rule6 % int2)) triple3) -> (rule8 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3
Gary is not quiet.
False
5
inv-proof
[(((((((triple3) -> rule3)) -> rule6) triple3) -> rule8))]
("Gary" "is" "quiet" "-")
((((((triple3) -> (rule3 % int3))) -> (rule6 % int2)) triple3) -> (rule8 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3
Gary is not green.
Unknown
inv-rconc
[@1: Gary is green.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Gary" "is" "green" "-")
Dave is furry.
Unknown
rconc
[@1: Dave is furry.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "furry" "+")
Dave is not kind.
Unknown
inv-rconc
[@1: Dave is kind.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Dave" "is" "kind" "-")
Erin is furry.
Unknown
rconc
[@1: Erin is furry.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Erin" "is" "furry" "+")
Erin is not round.
Unknown
inv-random
[@0: Erin is round.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "round" "-")
Erin is white.
Unknown
random
[@0: Erin is white.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "white" "+")
Gary is not round.
Unknown
inv-random
[@0: Gary is round.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "round" "-")
Dave is white.
Unknown
random
[@0: Dave is white.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "white" "+")
@0: Dave is green.[(triple1)] Erin is nice.[(triple2)] Gary is white.[(triple3)] Harry is kind.[(triple4)] @1: Gary is furry.[(((triple3) -> rule3))] @2: Gary is nice.[(((((triple3) -> rule3)) -> rule6))] @3: Gary is quiet.[(((((((triple3) -> rule3)) -> rule6) triple3) -> rule8))]
Dave is green.
("Dave" "is" "green" "+")
triple1
Erin is nice.
("Erin" "is" "nice" "+")
triple2
Gary is white.
("Gary" "is" "white" "+")
triple3
Harry is kind.
("Harry" "is" "kind" "+")
triple4
Gary is furry.
("Gary" "is" "furry" "+")
((triple3) -> (rule3 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
((((triple3) -> (rule3 % int2))) -> (rule6 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
((((((triple3) -> (rule3 % int3))) -> (rule6 % int2)) triple3) -> (rule8 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3