Dave is cold. Gary is kind. Gary is rough. Furry things are quiet. All kind things are rough. If something is furry and big then it is rough. All furry things are kind. All cold things are furry. If Gary is not cold then Gary is furry.
Dave is cold.
("Dave" "is" "cold" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Furry things are quiet.
((("something" "is" "furry" "+")) -> ("something" "is" "quiet" "+"))
All kind things are rough.
((("something" "is" "kind" "+")) -> ("something" "is" "rough" "+"))
If something is furry and big then it is rough.
((("something" "is" "furry" "+") ("something" "is" "big" "+")) -> ("something" "is" "rough" "+"))
All furry things are kind.
((("something" "is" "furry" "+")) -> ("something" "is" "kind" "+"))
All cold things are furry.
((("something" "is" "cold" "+")) -> ("something" "is" "furry" "+"))
If Gary is not cold then Gary is furry.
((("Gary" "is" "cold" "~")) -> ("Gary" "is" "furry" "+"))
Gary is rough.
True
1
proof
[(triple3 OR ((triple2) -> rule2))]
("Gary" "is" "rough" "+")
triple3
((triple2) -> (rule2 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is not rough.
False
1
inv-proof
[(triple3 OR ((triple2) -> rule2))]
("Gary" "is" "rough" "-")
triple3
((triple2) -> (rule2 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Dave is furry.
True
2
proof
[(((triple1) -> rule5))]
("Dave" "is" "furry" "+")
((triple1) -> (rule5 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is not furry.
False
2
inv-proof
[(((triple1) -> rule5))]
("Dave" "is" "furry" "-")
((triple1) -> (rule5 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is quiet.
True
3
proof
[(((((triple1) -> rule5)) -> rule1))]
("Dave" "is" "quiet" "+")
((((triple1) -> (rule5 % int2))) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is not kind.
False
3
inv-proof
[(((((triple1) -> rule5)) -> rule4))]
("Dave" "is" "kind" "-")
((((triple1) -> (rule5 % int2))) -> (rule4 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is rough.
True
4
proof
[(((((((triple1) -> rule5)) -> rule4)) -> rule2))]
("Dave" "is" "rough" "+")
((((((triple1) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Dave is not rough.
False
4
inv-proof
[(((((((triple1) -> rule5)) -> rule4)) -> rule2))]
("Dave" "is" "rough" "-")
((((((triple1) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Gary is not quiet.
Unknown
inv-rconc
[@2: Gary is quiet.[CWA. Example of deepest failure = (rule1 <- rule5 <- FAIL)]]
("Gary" "is" "quiet" "-")
Gary is furry.
Unknown
rconc
[@1: Gary is furry.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Gary" "is" "furry" "+")
Gary is not nice.
Unknown
inv-random
[@0: Gary is nice.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "nice" "-")
Dave is nice.
Unknown
random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "+")
Gary is not cold.
Unknown
inv-random
[@0: Gary is cold.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "cold" "-")
Dave is big.
Unknown
random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "+")
@0: Dave is cold.[(triple1)] Gary is kind.[(triple2)] Gary is rough.[(triple3 OR ((triple2) -> rule2))] @1: Dave is furry.[(((triple1) -> rule5))] @2: Dave is kind.[(((((triple1) -> rule5)) -> rule4))] Dave is quiet.[(((((triple1) -> rule5)) -> rule1))] @3: Dave is rough.[(((((((triple1) -> rule5)) -> rule4)) -> rule2))]
Dave is cold.
("Dave" "is" "cold" "+")
triple1
Gary is kind.
("Gary" "is" "kind" "+")
triple2
Gary is rough.
("Gary" "is" "rough" "+")
triple3
((triple2) -> (rule2 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
((triple1) -> (rule5 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
((((triple1) -> (rule5 % int2))) -> (rule4 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
((((triple1) -> (rule5 % int2))) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
((((((triple1) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3