Bob is furry. Dave is white. Gary is blue. Big things are not white. Kind things are smart. All furry things are kind. Furry, kind things are rough. If something is white and not kind then it is not rough. If something is rough and smart then it is not blue.
Bob is furry.
("Bob" "is" "furry" "+")
Dave is white.
("Dave" "is" "white" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Big things are not white.
((("something" "is" "big" "+")) -> ("something" "is" "white" "-"))
Kind things are smart.
((("something" "is" "kind" "+")) -> ("something" "is" "smart" "+"))
All furry things are kind.
((("something" "is" "furry" "+")) -> ("something" "is" "kind" "+"))
Furry, kind things are rough.
((("something" "is" "furry" "+") ("something" "is" "kind" "+")) -> ("something" "is" "rough" "+"))
If something is white and not kind then it is not rough.
((("something" "is" "white" "+") ("something" "is" "kind" "~")) -> ("something" "is" "rough" "-"))
If something is rough and smart then it is not blue.
((("something" "is" "rough" "+") ("something" "is" "smart" "+")) -> ("something" "is" "blue" "-"))
Bob is furry.
True
1
proof
[(triple1)]
("Bob" "is" "furry" "+")
triple1
Gary is not blue.
False
1
inv-proof
[(triple3)]
("Gary" "is" "blue" "-")
triple3
Bob is kind.
True
2
proof
[(((triple1) -> rule3))]
("Bob" "is" "kind" "+")
((triple1) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is not kind.
False
2
inv-proof
[(((triple1) -> rule3))]
("Bob" "is" "kind" "-")
((triple1) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is smart.
True
3
proof
[(((((triple1) -> rule3)) -> rule2))]
("Bob" "is" "smart" "+")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is not smart.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule2))]
("Bob" "is" "smart" "-")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is not blue.
True
8
proof
[(((((triple1 ((triple1) -> rule3)) -> rule4) ((((triple1) -> rule3)) -> rule2)) -> rule6))]
("Bob" "is" "blue" "-")
((((triple1 ((triple1) -> (rule3 % int4))) -> (rule4 % int3)) ((((triple1) -> (rule3 % int4))) -> (rule2 % int2))) -> (rule6 % int1))
Bob is not blue.
("Bob" "is" "blue" "-")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
Bob is kind.
("Bob" "is" "kind" "+")
int4
Bob is blue.
False
8
inv-proof
[(((((triple1 ((triple1) -> rule3)) -> rule4) ((((triple1) -> rule3)) -> rule2)) -> rule6))]
("Bob" "is" "blue" "+")
((((triple1 ((triple1) -> (rule3 % int4))) -> (rule4 % int3)) ((((triple1) -> (rule3 % int4))) -> (rule2 % int2))) -> (rule6 % int1))
Bob is not blue.
("Bob" "is" "blue" "-")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
Bob is kind.
("Bob" "is" "kind" "+")
int4
Dave is not rough.
Unknown
inv-rconc
[@1: Dave is rough.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Dave" "is" "rough" "-")
Gary is kind.
Unknown
rconc
[@1: Gary is kind.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "kind" "+")
Gary is not smart.
Unknown
inv-rconc
[@2: Gary is smart.[CWA. Example of deepest failure = (rule2 <- rule3 <- FAIL)]]
("Gary" "is" "smart" "-")
Dave is smart.
Unknown
rconc
[@2: Dave is smart.[CWA. Example of deepest failure = (rule2 <- rule3 <- FAIL)]]
("Dave" "is" "smart" "+")
Dave is not big.
Unknown
inv-random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "-")
Gary is white.
Unknown
random
[@0: Gary is white.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "white" "+")
Bob is not big.
Unknown
inv-random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "-")
Dave is furry.
Unknown
random
[@0: Dave is furry.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "furry" "+")
@0: Bob is furry.[(triple1)] Dave is white.[(triple2)] Gary is blue.[(triple3)] @1: Bob is kind.[(((triple1) -> rule3))] @2: Bob is rough.[(((triple1 ((triple1) -> rule3)) -> rule4))] Bob is smart.[(((((triple1) -> rule3)) -> rule2))] @3: Bob is not blue.[(((((triple1 ((triple1) -> rule3)) -> rule4) ((((triple1) -> rule3)) -> rule2)) -> rule6))]
Bob is furry.
("Bob" "is" "furry" "+")
triple1
Dave is white.
("Dave" "is" "white" "+")
triple2
Gary is blue.
("Gary" "is" "blue" "+")
triple3
Bob is kind.
("Bob" "is" "kind" "+")
((triple1) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
((triple1 ((triple1) -> (rule3 % int2))) -> (rule4 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is not blue.
("Bob" "is" "blue" "-")
((((triple1 ((triple1) -> (rule3 % int4))) -> (rule4 % int3)) ((((triple1) -> (rule3 % int4))) -> (rule2 % int2))) -> (rule6 % int1))
Bob is not blue.
("Bob" "is" "blue" "-")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
Bob is kind.
("Bob" "is" "kind" "+")
int4