Anne is furry. Bob is young. If something is furry then it is round. If something is furry then it is young. If Anne is furry and Anne is young then Anne is white. All furry things are nice. If Bob is young then Bob is nice. If something is round and nice then it is young. If something is nice then it is white. White, nice things are smart.
Anne is furry.
("Anne" "is" "furry" "+")
Bob is young.
("Bob" "is" "young" "+")
If something is furry then it is round.
((("something" "is" "furry" "+")) -> ("something" "is" "round" "+"))
If something is furry then it is young.
((("something" "is" "furry" "+")) -> ("something" "is" "young" "+"))
If Anne is furry and Anne is young then Anne is white.
((("Anne" "is" "furry" "+") ("Anne" "is" "young" "+")) -> ("Anne" "is" "white" "+"))
All furry things are nice.
((("something" "is" "furry" "+")) -> ("something" "is" "nice" "+"))
If Bob is young then Bob is nice.
((("Bob" "is" "young" "+")) -> ("Bob" "is" "nice" "+"))
If something is round and nice then it is young.
((("something" "is" "round" "+") ("something" "is" "nice" "+")) -> ("something" "is" "young" "+"))
If something is nice then it is white.
((("something" "is" "nice" "+")) -> ("something" "is" "white" "+"))
White, nice things are smart.
((("something" "is" "white" "+") ("something" "is" "nice" "+")) -> ("something" "is" "smart" "+"))
Anne is furry.
True
1
proof
[(triple1)]
("Anne" "is" "furry" "+")
triple1
Bob is not young.
False
1
inv-proof
[(triple2)]
("Bob" "is" "young" "-")
triple2
Anne is round.
True
2
proof
[(((triple1) -> rule1))]
("Anne" "is" "round" "+")
((triple1) -> (rule1 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is not nice.
False
2
inv-proof
[(((triple1) -> rule4))]
("Anne" "is" "nice" "-")
((triple1) -> (rule4 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is white.
True
3
proof
[(((((triple1) -> rule4)) -> rule7) OR ((triple1 ((triple1) -> rule2)) -> rule3) OR ((triple1 ((((triple1) -> rule1) ((triple1) -> rule4)) -> rule6)) -> rule3))]
("Anne" "is" "white" "+")
((((triple1) -> (rule4 % int2))) -> (rule7 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
((triple1 ((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
((triple1 ((((triple1) -> (rule1 % int4)) ((triple1) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Anne is round.
("Anne" "is" "round" "+")
int4
Anne is not white.
False
3
inv-proof
[(((((triple1) -> rule4)) -> rule7) OR ((triple1 ((triple1) -> rule2)) -> rule3) OR ((triple1 ((((triple1) -> rule1) ((triple1) -> rule4)) -> rule6)) -> rule3))]
("Anne" "is" "white" "-")
((((triple1) -> (rule4 % int2))) -> (rule7 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
((triple1 ((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
((triple1 ((((triple1) -> (rule1 % int4)) ((triple1) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Anne is round.
("Anne" "is" "round" "+")
int4
Bob is not round.
Unknown
inv-rconc
[@1: Bob is round.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "round" "-")
Anne is red.
Unknown
random
[@0: Anne is red.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "red" "+")
Bob is not red.
Unknown
inv-random
[@0: Bob is red.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "red" "-")
Bob is furry.
Unknown
random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "+")
@0: Anne is furry.[(triple1)] Bob is young.[(triple2)] @1: Anne is nice.[(((triple1) -> rule4))] Anne is round.[(((triple1) -> rule1))] Anne is young.[(((triple1) -> rule2) OR ((((triple1) -> rule1) ((triple1) -> rule4)) -> rule6))] Bob is nice.[(((triple2) -> rule5))] @2: Anne is white.[(((((triple1) -> rule4)) -> rule7) OR ((triple1 ((triple1) -> rule2)) -> rule3) OR ((triple1 ((((triple1) -> rule1) ((triple1) -> rule4)) -> rule6)) -> rule3))] Bob is white.[(((((triple2) -> rule5)) -> rule7))] @3: Anne is smart.[(((((((triple1) -> rule4)) -> rule7) ((triple1) -> rule4)) -> rule8) OR ((((triple1 ((triple1) -> rule2)) -> rule3) ((triple1) -> rule4)) -> rule8) OR ((((triple1 ((((triple1) -> rule1) ((triple1) -> rule4)) -> rule6)) -> rule3) ((triple1) -> rule4)) -> rule8))] Bob is smart.[(((((((triple2) -> rule5)) -> rule7) ((triple2) -> rule5)) -> rule8))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Bob is young.
("Bob" "is" "young" "+")
triple2
Anne is nice.
("Anne" "is" "nice" "+")
((triple1) -> (rule4 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
((triple1) -> (rule1 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
((triple1) -> (rule2 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
((((triple1) -> (rule1 % int3)) ((triple1) -> (rule4 % int2))) -> (rule6 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
Bob is nice.
("Bob" "is" "nice" "+")
((triple2) -> (rule5 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
((((triple1) -> (rule4 % int2))) -> (rule7 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
((triple1 ((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
((triple1 ((((triple1) -> (rule1 % int4)) ((triple1) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Anne is round.
("Anne" "is" "round" "+")
int4
Bob is white.
("Bob" "is" "white" "+")
((((triple2) -> (rule5 % int2))) -> (rule7 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
((((((triple1) -> (rule4 % int3))) -> (rule7 % int2)) ((triple1) -> (rule4 % int3))) -> (rule8 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
((((triple1 ((triple1) -> (rule2 % int4))) -> (rule3 % int3)) ((triple1) -> (rule4 % int2))) -> (rule8 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
Anne is young.
("Anne" "is" "young" "+")
int4
((((triple1 ((((triple1) -> (rule1 % int5)) ((triple1) -> (rule4 % int4))) -> (rule6 % int3))) -> (rule3 % int2)) ((triple1) -> (rule4 % int4))) -> (rule8 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Anne is nice.
("Anne" "is" "nice" "+")
int4
Anne is round.
("Anne" "is" "round" "+")
int5
Bob is smart.
("Bob" "is" "smart" "+")
((((((triple2) -> (rule5 % int3))) -> (rule7 % int2)) ((triple2) -> (rule5 % int3))) -> (rule8 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
int3