Bob is furry. Dave is green. If something is green and furry then it is quiet. Green things are quiet. If something is green and smart then it is kind. If something is big and not green then it is kind. If something is green and white then it is big. If something is quiet then it is big. Big, green things are not white. If Bob is green then Bob is furry.
Bob is furry.
("Bob" "is" "furry" "+")
Dave is green.
("Dave" "is" "green" "+")
If something is green and furry then it is quiet.
((("something" "is" "green" "+") ("something" "is" "furry" "+")) -> ("something" "is" "quiet" "+"))
Green things are quiet.
((("something" "is" "green" "+")) -> ("something" "is" "quiet" "+"))
If something is green and smart then it is kind.
((("something" "is" "green" "+") ("something" "is" "smart" "+")) -> ("something" "is" "kind" "+"))
If something is big and not green then it is kind.
((("something" "is" "big" "+") ("something" "is" "green" "~")) -> ("something" "is" "kind" "+"))
If something is green and white then it is big.
((("something" "is" "green" "+") ("something" "is" "white" "+")) -> ("something" "is" "big" "+"))
If something is quiet then it is big.
((("something" "is" "quiet" "+")) -> ("something" "is" "big" "+"))
Big, green things are not white.
((("something" "is" "big" "+") ("something" "is" "green" "+")) -> ("something" "is" "white" "-"))
If Bob is green then Bob is furry.
((("Bob" "is" "green" "+")) -> ("Bob" "is" "furry" "+"))
Dave is green.
True
1
proof
[(triple2)]
("Dave" "is" "green" "+")
triple2
Bob is not furry.
False
1
inv-proof
[(triple1)]
("Bob" "is" "furry" "-")
triple1
Dave is quiet.
True
2
proof
[(((triple2) -> rule2))]
("Dave" "is" "quiet" "+")
((triple2) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is not quiet.
False
2
inv-proof
[(((triple2) -> rule2))]
("Dave" "is" "quiet" "-")
((triple2) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is big.
True
3
proof
[(((((triple2) -> rule2)) -> rule6))]
("Dave" "is" "big" "+")
((((triple2) -> (rule2 % int2))) -> (rule6 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is not big.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule6))]
("Dave" "is" "big" "-")
((((triple2) -> (rule2 % int2))) -> (rule6 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is not white.
True
5
proof
[(((((((triple2) -> rule2)) -> rule6) triple2) -> rule7))]
("Dave" "is" "white" "-")
((((((triple2) -> (rule2 % int3))) -> (rule6 % int2)) triple2) -> (rule7 % int1))
Dave is not white.
("Dave" "is" "white" "-")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Dave is white.
False
5
inv-proof
[(((((((triple2) -> rule2)) -> rule6) triple2) -> rule7))]
("Dave" "is" "white" "+")
((((((triple2) -> (rule2 % int3))) -> (rule6 % int2)) triple2) -> (rule7 % int1))
Dave is not white.
("Dave" "is" "white" "-")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Bob is not quiet.
Unknown
inv-rconc
[@1: Bob is quiet.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "quiet" "-")
Dave is kind.
Unknown
rconc
[@1: Dave is kind.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "kind" "+")
Bob is not kind.
Unknown
inv-rconc
[@1: Bob is kind.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "kind" "-")
Bob is big.
Unknown
rconc
[@2: Bob is big.[CWA. Example of deepest failure = (rule6 <- rule1 <- FAIL)]]
("Bob" "is" "big" "+")
Bob is not green.
Unknown
inv-random
[@0: Bob is green.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "green" "-")
Dave is smart.
Unknown
random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "+")
Bob is not smart.
Unknown
inv-random
[@0: Bob is smart.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "smart" "-")
Bob is white.
Unknown
random
[@0: Bob is white.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "white" "+")
@0: Bob is furry.[(triple1)] Dave is green.[(triple2)] @1: Dave is quiet.[(((triple2) -> rule2))] @2: Dave is big.[(((((triple2) -> rule2)) -> rule6))] @3: Dave is not white.[(((((((triple2) -> rule2)) -> rule6) triple2) -> rule7))]
Bob is furry.
("Bob" "is" "furry" "+")
triple1
Dave is green.
("Dave" "is" "green" "+")
triple2
Dave is quiet.
("Dave" "is" "quiet" "+")
((triple2) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
((((triple2) -> (rule2 % int2))) -> (rule6 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is not white.
("Dave" "is" "white" "-")
((((((triple2) -> (rule2 % int3))) -> (rule6 % int2)) triple2) -> (rule7 % int1))
Dave is not white.
("Dave" "is" "white" "-")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3