Bob is furry. If Bob is furry then Bob is big. All kind things are white. Rough, kind things are not white. Green, kind things are white. All furry, blue things are kind. All rough, furry things are not green. If Bob is big then Bob is blue. All green things are rough.
Bob is furry.
("Bob" "is" "furry" "+")
If Bob is furry then Bob is big.
((("Bob" "is" "furry" "+")) -> ("Bob" "is" "big" "+"))
All kind things are white.
((("something" "is" "kind" "+")) -> ("something" "is" "white" "+"))
Rough, kind things are not white.
((("something" "is" "rough" "+") ("something" "is" "kind" "+")) -> ("something" "is" "white" "-"))
Green, kind things are white.
((("something" "is" "green" "+") ("something" "is" "kind" "+")) -> ("something" "is" "white" "+"))
All furry, blue things are kind.
((("something" "is" "furry" "+") ("something" "is" "blue" "+")) -> ("something" "is" "kind" "+"))
All rough, furry things are not green.
((("something" "is" "rough" "+") ("something" "is" "furry" "+")) -> ("something" "is" "green" "-"))
If Bob is big then Bob is blue.
((("Bob" "is" "big" "+")) -> ("Bob" "is" "blue" "+"))
All green things are rough.
((("something" "is" "green" "+")) -> ("something" "is" "rough" "+"))
Bob is furry.
True
1
proof
[(triple1)]
("Bob" "is" "furry" "+")
triple1
Bob is not furry.
False
1
inv-proof
[(triple1)]
("Bob" "is" "furry" "-")
triple1
Bob is big.
True
2
proof
[(((triple1) -> rule1))]
("Bob" "is" "big" "+")
((triple1) -> (rule1 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is not big.
False
2
inv-proof
[(((triple1) -> rule1))]
("Bob" "is" "big" "-")
((triple1) -> (rule1 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is blue.
True
3
proof
[(((((triple1) -> rule1)) -> rule7))]
("Bob" "is" "blue" "+")
((((triple1) -> (rule1 % int2))) -> (rule7 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is not blue.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule7))]
("Bob" "is" "blue" "-")
((((triple1) -> (rule1 % int2))) -> (rule7 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is not rough.
Unknown
inv-rconc
[@1: Bob is rough.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Bob" "is" "rough" "-")
Bob is green.
Unknown
random
[@0: Bob is green.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "green" "+")
@0: Bob is furry.[(triple1)] @1: Bob is big.[(((triple1) -> rule1))] @2: Bob is blue.[(((((triple1) -> rule1)) -> rule7))] @3: Bob is kind.[(((triple1 ((((triple1) -> rule1)) -> rule7)) -> rule5))] @4: Bob is white.[(((((triple1 ((((triple1) -> rule1)) -> rule7)) -> rule5)) -> rule2))]
Bob is furry.
("Bob" "is" "furry" "+")
triple1
Bob is big.
("Bob" "is" "big" "+")
((triple1) -> (rule1 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
((((triple1) -> (rule1 % int2))) -> (rule7 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
((triple1 ((((triple1) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
((((triple1 ((((triple1) -> (rule1 % int4))) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Bob is big.
("Bob" "is" "big" "+")
int4