Anne is furry. Anne is kind. Anne is not quiet. Bob is kind. Bob is young. Fiona is big. Fiona is nice. If Anne is young then Anne is not nice. Young things are not furry. If something is round and not furry then it is big. If something is big then it is nice. If something is young and quiet then it is kind. If something is big then it is quiet. Kind things are round. Furry, nice things are round.
Anne is furry.
("Anne" "is" "furry" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is not quiet.
("Anne" "is" "quiet" "-")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is young.
("Bob" "is" "young" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
If Anne is young then Anne is not nice.
((("Anne" "is" "young" "+")) -> ("Anne" "is" "nice" "-"))
Young things are not furry.
((("something" "is" "young" "+")) -> ("something" "is" "furry" "-"))
If something is round and not furry then it is big.
((("something" "is" "round" "+") ("something" "is" "furry" "~")) -> ("something" "is" "big" "+"))
If something is big then it is nice.
((("something" "is" "big" "+")) -> ("something" "is" "nice" "+"))
If something is young and quiet then it is kind.
((("something" "is" "young" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "kind" "+"))
If something is big then it is quiet.
((("something" "is" "big" "+")) -> ("something" "is" "quiet" "+"))
Kind things are round.
((("something" "is" "kind" "+")) -> ("something" "is" "round" "+"))
Furry, nice things are round.
((("something" "is" "furry" "+") ("something" "is" "nice" "+")) -> ("something" "is" "round" "+"))
Bob is young.
True
1
proof
[(triple5)]
("Bob" "is" "young" "+")
triple5
Anne is not furry.
False
1
inv-proof
[(triple1)]
("Anne" "is" "furry" "-")
triple1
Anne is round.
True
2
proof
[(((triple2) -> rule7))]
("Anne" "is" "round" "+")
((triple2) -> (rule7 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Bob is not round.
False
2
inv-proof
[(((triple4) -> rule7))]
("Bob" "is" "round" "-")
((triple4) -> (rule7 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is big.
True
5
proof
[(((((triple4) -> rule7) ((triple5) -> rule2)) -> rule3))]
("Bob" "is" "big" "+")
((((triple4) -> (rule7 % int3)) ((triple5) -> (rule2 % int2))) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is not furry.
("Bob" "is" "furry" "-")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Bob is not big.
False
5
inv-proof
[(((((triple4) -> rule7) ((triple5) -> rule2)) -> rule3))]
("Bob" "is" "big" "-")
((((triple4) -> (rule7 % int3)) ((triple5) -> (rule2 % int2))) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is not furry.
("Bob" "is" "furry" "-")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Bob is quiet.
True
6
proof
[(((((((triple4) -> rule7) ((triple5) -> rule2)) -> rule3)) -> rule6))]
("Bob" "is" "quiet" "+")
((((((triple4) -> (rule7 % int4)) ((triple5) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is not furry.
("Bob" "is" "furry" "-")
int3
Bob is round.
("Bob" "is" "round" "+")
int4
Bob is not nice.
False
6
inv-proof
[(((((((triple4) -> rule7) ((triple5) -> rule2)) -> rule3)) -> rule4))]
("Bob" "is" "nice" "-")
((((((triple4) -> (rule7 % int4)) ((triple5) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is not furry.
("Bob" "is" "furry" "-")
int3
Bob is round.
("Bob" "is" "round" "+")
int4
Anne is not big.
Unknown
inv-rconc
[@1: Anne is big.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Anne" "is" "big" "-")
Fiona is round.
Unknown
rconc
[@2: Fiona is round.[CWA. Example of deepest failure = (rule7 <- rule5 <- FAIL)]]
("Fiona" "is" "round" "+")
Anne is not nice.
Unknown
inv-rconc
[@2: Anne is nice.[CWA. Example of deepest failure = (rule4 <- rule3 <- FAIL)]]
("Anne" "is" "nice" "-")
Fiona is kind.
Unknown
rconc
[@1: Fiona is kind.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Fiona" "is" "kind" "+")
Anne is not young.
Unknown
inv-random
[@0: Anne is young.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "young" "-")
Fiona is young.
Unknown
random
[@0: Fiona is young.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "young" "+")
@0: Anne is furry.[(triple1)] Anne is kind.[(triple2)] Anne is not quiet.[(triple3)] Bob is kind.[(triple4)] Bob is young.[(triple5)] Fiona is big.[(triple6)] Fiona is nice.[(triple7 OR ((triple6) -> rule4))] @1: Anne is round.[(((triple2) -> rule7))] Bob is not furry.[(((triple5) -> rule2))] Bob is round.[(((triple4) -> rule7))] Fiona is quiet.[(((triple6) -> rule6))] @2: Bob is big.[(((((triple4) -> rule7) ((triple5) -> rule2)) -> rule3))] @3: Bob is nice.[(((((((triple4) -> rule7) ((triple5) -> rule2)) -> rule3)) -> rule4))] Bob is quiet.[(((((((triple4) -> rule7) ((triple5) -> rule2)) -> rule3)) -> rule6))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Anne is kind.
("Anne" "is" "kind" "+")
triple2
Anne is not quiet.
("Anne" "is" "quiet" "-")
triple3
Bob is kind.
("Bob" "is" "kind" "+")
triple4
Bob is young.
("Bob" "is" "young" "+")
triple5
Fiona is big.
("Fiona" "is" "big" "+")
triple6
Fiona is nice.
("Fiona" "is" "nice" "+")
triple7
((triple6) -> (rule4 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
((triple2) -> (rule7 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Bob is not furry.
("Bob" "is" "furry" "-")
((triple5) -> (rule2 % int1))
Bob is not furry.
("Bob" "is" "furry" "-")
int1
Bob is round.
("Bob" "is" "round" "+")
((triple4) -> (rule7 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
((triple6) -> (rule6 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
((((triple4) -> (rule7 % int3)) ((triple5) -> (rule2 % int2))) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is not furry.
("Bob" "is" "furry" "-")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Bob is nice.
("Bob" "is" "nice" "+")
((((((triple4) -> (rule7 % int4)) ((triple5) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is not furry.
("Bob" "is" "furry" "-")
int3
Bob is round.
("Bob" "is" "round" "+")
int4
Bob is quiet.
("Bob" "is" "quiet" "+")
((((((triple4) -> (rule7 % int4)) ((triple5) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is not furry.
("Bob" "is" "furry" "-")
int3
Bob is round.
("Bob" "is" "round" "+")
int4