Anne is round. Bob is furry. Dave is white. If Anne is smart and Anne is not furry then Anne is young. All round things are big. If something is round and not white then it is young. If something is furry and white then it is young. Big things are smart. If Dave is white then Dave is young. Smart things are kind. If Dave is white then Dave is not furry.
Anne is round.
("Anne" "is" "round" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Dave is white.
("Dave" "is" "white" "+")
If Anne is smart and Anne is not furry then Anne is young.
((("Anne" "is" "smart" "+") ("Anne" "is" "furry" "~")) -> ("Anne" "is" "young" "+"))
All round things are big.
((("something" "is" "round" "+")) -> ("something" "is" "big" "+"))
If something is round and not white then it is young.
((("something" "is" "round" "+") ("something" "is" "white" "~")) -> ("something" "is" "young" "+"))
If something is furry and white then it is young.
((("something" "is" "furry" "+") ("something" "is" "white" "+")) -> ("something" "is" "young" "+"))
Big things are smart.
((("something" "is" "big" "+")) -> ("something" "is" "smart" "+"))
If Dave is white then Dave is young.
((("Dave" "is" "white" "+")) -> ("Dave" "is" "young" "+"))
Smart things are kind.
((("something" "is" "smart" "+")) -> ("something" "is" "kind" "+"))
If Dave is white then Dave is not furry.
((("Dave" "is" "white" "+")) -> ("Dave" "is" "furry" "-"))
Dave is white.
True
1
proof
[(triple3)]
("Dave" "is" "white" "+")
triple3
Dave is not white.
False
1
inv-proof
[(triple3)]
("Dave" "is" "white" "-")
triple3
Anne is big.
True
2
proof
[(((triple1) -> rule2))]
("Anne" "is" "big" "+")
((triple1) -> (rule2 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Dave is not young.
False
2
inv-proof
[(((triple3) -> rule6))]
("Dave" "is" "young" "-")
((triple3) -> (rule6 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Anne is smart.
True
3
proof
[(((((triple1) -> rule2)) -> rule5))]
("Anne" "is" "smart" "+")
((((triple1) -> (rule2 % int2))) -> (rule5 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is not smart.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule5))]
("Anne" "is" "smart" "-")
((((triple1) -> (rule2 % int2))) -> (rule5 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is kind.
True
4
proof
[(((((((triple1) -> rule2)) -> rule5)) -> rule7))]
("Anne" "is" "kind" "+")
((((((triple1) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
Anne is not kind.
False
4
inv-proof
[(((((((triple1) -> rule2)) -> rule5)) -> rule7))]
("Anne" "is" "kind" "-")
((((((triple1) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
Dave is not kind.
Unknown
inv-rconc
[@3: Dave is kind.[CWA. Example of deepest failure = (rule7 <- rule5 <- rule2 <- FAIL)]]
("Dave" "is" "kind" "-")
Bob is big.
Unknown
rconc
[@1: Bob is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "big" "+")
Bob is not smart.
Unknown
inv-rconc
[@2: Bob is smart.[CWA. Example of deepest failure = (rule5 <- rule2 <- FAIL)]]
("Bob" "is" "smart" "-")
Dave is big.
Unknown
rconc
[@1: Dave is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "big" "+")
Bob is not white.
Unknown
inv-random
[@0: Bob is white.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "white" "-")
Anne is white.
Unknown
random
[@0: Anne is white.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "white" "+")
Anne is not furry.
Unknown
inv-random
[@0: Anne is furry.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "furry" "-")
Dave is round.
Unknown
random
[@0: Dave is round.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "round" "+")
@0: Anne is round.[(triple1)] Bob is furry.[(triple2)] Dave is white.[(triple3)] @1: Anne is big.[(((triple1) -> rule2))] Dave is not furry.[(((triple3) -> rule8))] Dave is young.[(((triple3) -> rule6))] @2: Anne is smart.[(((((triple1) -> rule2)) -> rule5))] @3: Anne is kind.[(((((((triple1) -> rule2)) -> rule5)) -> rule7))]
Anne is round.
("Anne" "is" "round" "+")
triple1
Bob is furry.
("Bob" "is" "furry" "+")
triple2
Dave is white.
("Dave" "is" "white" "+")
triple3
Anne is big.
("Anne" "is" "big" "+")
((triple1) -> (rule2 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Dave is not furry.
("Dave" "is" "furry" "-")
((triple3) -> (rule8 % int1))
Dave is not furry.
("Dave" "is" "furry" "-")
int1
Dave is young.
("Dave" "is" "young" "+")
((triple3) -> (rule6 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
((((triple1) -> (rule2 % int2))) -> (rule5 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
((((((triple1) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3