Bob is not furry. Dave is green. Gary is round. Harry is kind. If Harry is smart then Harry is rough. All furry, green things are round. Furry things are green. If something is round then it is not blue. Green things are furry. If Bob is green then Bob is rough. Blue, smart things are kind. If Gary is round then Gary is furry.
Bob is not furry.
("Bob" "is" "furry" "-")
Dave is green.
("Dave" "is" "green" "+")
Gary is round.
("Gary" "is" "round" "+")
Harry is kind.
("Harry" "is" "kind" "+")
If Harry is smart then Harry is rough.
((("Harry" "is" "smart" "+")) -> ("Harry" "is" "rough" "+"))
All furry, green things are round.
((("something" "is" "furry" "+") ("something" "is" "green" "+")) -> ("something" "is" "round" "+"))
Furry things are green.
((("something" "is" "furry" "+")) -> ("something" "is" "green" "+"))
If something is round then it is not blue.
((("something" "is" "round" "+")) -> ("something" "is" "blue" "-"))
Green things are furry.
((("something" "is" "green" "+")) -> ("something" "is" "furry" "+"))
If Bob is green then Bob is rough.
((("Bob" "is" "green" "+")) -> ("Bob" "is" "rough" "+"))
Blue, smart things are kind.
((("something" "is" "blue" "+") ("something" "is" "smart" "+")) -> ("something" "is" "kind" "+"))
If Gary is round then Gary is furry.
((("Gary" "is" "round" "+")) -> ("Gary" "is" "furry" "+"))
Gary is round.
True
1
proof
[(triple3)]
("Gary" "is" "round" "+")
triple3
Gary is not round.
False
1
inv-proof
[(triple3)]
("Gary" "is" "round" "-")
triple3
Gary is not blue.
True
2
proof
[(((triple3) -> rule4))]
("Gary" "is" "blue" "-")
((triple3) -> (rule4 % int1))
Gary is not blue.
("Gary" "is" "blue" "-")
int1
Gary is blue.
False
2
inv-proof
[(((triple3) -> rule4))]
("Gary" "is" "blue" "+")
((triple3) -> (rule4 % int1))
Gary is not blue.
("Gary" "is" "blue" "-")
int1
Dave is round.
True
4
proof
[(((((triple2) -> rule5) triple2) -> rule2))]
("Dave" "is" "round" "+")
((((triple2) -> (rule5 % int2)) triple2) -> (rule2 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Gary is not green.
False
3
inv-proof
[(((((triple3) -> rule8)) -> rule3))]
("Gary" "is" "green" "-")
((((triple3) -> (rule8 % int2))) -> (rule3 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Dave is not blue.
True
5
proof
[(((((((triple2) -> rule5) triple2) -> rule2)) -> rule4))]
("Dave" "is" "blue" "-")
((((((triple2) -> (rule5 % int3)) triple2) -> (rule2 % int2))) -> (rule4 % int1))
Dave is not blue.
("Dave" "is" "blue" "-")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Dave is blue.
False
5
inv-proof
[(((((((triple2) -> rule5) triple2) -> rule2)) -> rule4))]
("Dave" "is" "blue" "+")
((((((triple2) -> (rule5 % int3)) triple2) -> (rule2 % int2))) -> (rule4 % int1))
Dave is not blue.
("Dave" "is" "blue" "-")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Harry is not rough.
Unknown
inv-rconc
[@1: Harry is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "rough" "-")
Bob is rough.
Unknown
rconc
[@2: Bob is rough.[CWA. Example of deepest failure = (rule6 <- rule3 <- FAIL)]]
("Bob" "is" "rough" "+")
Harry is not furry.
Unknown
inv-rconc
[@2: Harry is furry.[CWA. Example of deepest failure = (rule5 <- rule3 <- FAIL)]]
("Harry" "is" "furry" "-")
Harry is round.
Unknown
rconc
[@3: Harry is round.[CWA. Example of deepest failure = (rule2 <- rule5 <- rule3 <- FAIL)]]
("Harry" "is" "round" "+")
Dave is not smart.
Unknown
inv-random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "-")
Gary is rough.
Unknown
random
[@0: Gary is rough.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "rough" "+")
Harry is not blue.
Unknown
inv-random
[@0: Harry is blue.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "blue" "-")
Bob is blue.
Unknown
random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "+")
@0: Bob is not furry.[(triple1)] Dave is green.[(triple2)] Gary is round.[(triple3)] Harry is kind.[(triple4)] @1: Dave is furry.[(((triple2) -> rule5))] Gary is furry.[(((triple3) -> rule8))] Gary is not blue.[(((triple3) -> rule4))] @2: Dave is round.[(((((triple2) -> rule5) triple2) -> rule2))] Gary is green.[(((((triple3) -> rule8)) -> rule3))] @3: Dave is not blue.[(((((((triple2) -> rule5) triple2) -> rule2)) -> rule4))]
Bob is not furry.
("Bob" "is" "furry" "-")
triple1
Dave is green.
("Dave" "is" "green" "+")
triple2
Gary is round.
("Gary" "is" "round" "+")
triple3
Harry is kind.
("Harry" "is" "kind" "+")
triple4
Dave is furry.
("Dave" "is" "furry" "+")
((triple2) -> (rule5 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
((triple3) -> (rule8 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is not blue.
("Gary" "is" "blue" "-")
((triple3) -> (rule4 % int1))
Gary is not blue.
("Gary" "is" "blue" "-")
int1
Dave is round.
("Dave" "is" "round" "+")
((((triple2) -> (rule5 % int2)) triple2) -> (rule2 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
((((triple3) -> (rule8 % int2))) -> (rule3 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Dave is not blue.
("Dave" "is" "blue" "-")
((((((triple2) -> (rule5 % int3)) triple2) -> (rule2 % int2))) -> (rule4 % int1))
Dave is not blue.
("Dave" "is" "blue" "-")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3