Anne is quiet. Bob is young. Fiona is quiet. All nice people are young. Nice people are furry. All young people are nice. All nice people are kind. If someone is nice then they are kind. If someone is young then they are quiet. Kind people are smart. If someone is blue and nice then they are young.
Anne is quiet.
("Anne" "is" "quiet" "+")
Bob is young.
("Bob" "is" "young" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
All nice people are young.
((("someone" "is" "nice" "+")) -> ("someone" "is" "young" "+"))
Nice people are furry.
((("someone" "is" "nice" "+")) -> ("someone" "is" "furry" "+"))
All young people are nice.
((("someone" "is" "young" "+")) -> ("someone" "is" "nice" "+"))
All nice people are kind.
((("someone" "is" "nice" "+")) -> ("someone" "is" "kind" "+"))
If someone is nice then they are kind.
((("someone" "is" "nice" "+")) -> ("someone" "is" "kind" "+"))
If someone is young then they are quiet.
((("someone" "is" "young" "+")) -> ("someone" "is" "quiet" "+"))
Kind people are smart.
((("someone" "is" "kind" "+")) -> ("someone" "is" "smart" "+"))
If someone is blue and nice then they are young.
((("someone" "is" "blue" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "young" "+"))
Fiona is quiet.
True
1
proof
[(triple3)]
("Fiona" "is" "quiet" "+")
triple3
Anne is not quiet.
False
1
inv-proof
[(triple1)]
("Anne" "is" "quiet" "-")
triple1
Bob is quiet.
True
2
proof
[(((triple2) -> rule6))]
("Bob" "is" "quiet" "+")
((triple2) -> (rule6 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is not nice.
False
2
inv-proof
[(((triple2) -> rule3))]
("Bob" "is" "nice" "-")
((triple2) -> (rule3 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is furry.
True
3
proof
[(((((triple2) -> rule3)) -> rule2))]
("Bob" "is" "furry" "+")
((((triple2) -> (rule3 % int2))) -> (rule2 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is not furry.
False
3
inv-proof
[(((((triple2) -> rule3)) -> rule2))]
("Bob" "is" "furry" "-")
((((triple2) -> (rule3 % int2))) -> (rule2 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is smart.
True
4
proof
[(((((((triple2) -> rule3)) -> rule4)) -> rule7) OR ((((((triple2) -> rule3)) -> rule5)) -> rule7))]
("Bob" "is" "smart" "+")
((((((triple2) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
int3
((((((triple2) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
int3
Bob is not smart.
False
4
inv-proof
[(((((((triple2) -> rule3)) -> rule4)) -> rule7) OR ((((((triple2) -> rule3)) -> rule5)) -> rule7))]
("Bob" "is" "smart" "-")
((((((triple2) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
int3
((((((triple2) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
int3
Fiona is not smart.
Unknown
inv-rconc
[@4: Fiona is smart.[CWA. Example of deepest failure = (rule7 <- rule4 <- rule3 <- rule1 <- FAIL)]]
("Fiona" "is" "smart" "-")
Fiona is furry.
Unknown
rconc
[@3: Fiona is furry.[CWA. Example of deepest failure = (rule2 <- rule3 <- rule1 <- FAIL)]]
("Fiona" "is" "furry" "+")
Fiona is not nice.
Unknown
inv-rconc
[@2: Fiona is nice.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("Fiona" "is" "nice" "-")
Anne is young.
Unknown
rconc
[@3: Anne is young.[CWA. Example of deepest failure = (rule1 <- rule3 <- rule8 <- FAIL)]]
("Anne" "is" "young" "+")
Anne is not blue.
Unknown
inv-random
[@0: Anne is blue.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "blue" "-")
Bob is blue.
Unknown
random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "+")
@0: Anne is quiet.[(triple1)] Bob is young.[(triple2)] Fiona is quiet.[(triple3)] @1: Bob is nice.[(((triple2) -> rule3))] Bob is quiet.[(((triple2) -> rule6))] @2: Bob is furry.[(((((triple2) -> rule3)) -> rule2))] Bob is kind.[(((((triple2) -> rule3)) -> rule4) OR ((((triple2) -> rule3)) -> rule5))] @3: Bob is smart.[(((((((triple2) -> rule3)) -> rule4)) -> rule7) OR ((((((triple2) -> rule3)) -> rule5)) -> rule7))]
Anne is quiet.
("Anne" "is" "quiet" "+")
triple1
Bob is young.
("Bob" "is" "young" "+")
triple2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple3
Bob is nice.
("Bob" "is" "nice" "+")
((triple2) -> (rule3 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
((triple2) -> (rule6 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
((((triple2) -> (rule3 % int2))) -> (rule2 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
((((triple2) -> (rule3 % int2))) -> (rule4 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
((((triple2) -> (rule3 % int2))) -> (rule5 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
((((((triple2) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
int3
((((((triple2) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
int3