Anne is big. Anne is furry. Anne is quiet. Bob is furry. Bob is nice. Bob is quiet. Erin is not big. Erin is cold. Erin is furry. Erin is quiet. Erin is smart. Fiona is cold. Fiona is furry. Fiona is nice. Fiona is not young. If something is big then it is young. Big, furry things are quiet. If something is big and smart then it is cold. If something is smart and not big then it is nice. Young things are smart. If something is young and not quiet then it is smart.
Anne is big.
("Anne" "is" "big" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Erin is not big.
("Erin" "is" "big" "-")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is not young.
("Fiona" "is" "young" "-")
If something is big then it is young.
((("something" "is" "big" "+")) -> ("something" "is" "young" "+"))
Big, furry things are quiet.
((("something" "is" "big" "+") ("something" "is" "furry" "+")) -> ("something" "is" "quiet" "+"))
If something is big and smart then it is cold.
((("something" "is" "big" "+") ("something" "is" "smart" "+")) -> ("something" "is" "cold" "+"))
If something is smart and not big then it is nice.
((("something" "is" "smart" "+") ("something" "is" "big" "~")) -> ("something" "is" "nice" "+"))
Young things are smart.
((("something" "is" "young" "+")) -> ("something" "is" "smart" "+"))
If something is young and not quiet then it is smart.
((("something" "is" "young" "+") ("something" "is" "quiet" "~")) -> ("something" "is" "smart" "+"))
Erin is furry.
True
1
proof
[(triple9)]
("Erin" "is" "furry" "+")
triple9
Bob is not quiet.
False
1
inv-proof
[(triple6)]
("Bob" "is" "quiet" "-")
triple6
Anne is young.
True
2
proof
[(((triple1) -> rule1))]
("Anne" "is" "young" "+")
((triple1) -> (rule1 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Erin is not nice.
False
3
inv-proof
[(((triple11 triple7) -> rule4))]
("Erin" "is" "nice" "-")
((triple11 triple7) -> (rule4 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Anne is smart.
True
3
proof
[(((((triple1) -> rule1)) -> rule5))]
("Anne" "is" "smart" "+")
((((triple1) -> (rule1 % int2))) -> (rule5 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is not smart.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule5))]
("Anne" "is" "smart" "-")
((((triple1) -> (rule1 % int2))) -> (rule5 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is cold.
True
5
proof
[(((triple1 ((((triple1) -> rule1)) -> rule5)) -> rule3))]
("Anne" "is" "cold" "+")
((triple1 ((((triple1) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Anne is not cold.
False
5
inv-proof
[(((triple1 ((((triple1) -> rule1)) -> rule5)) -> rule3))]
("Anne" "is" "cold" "-")
((triple1 ((((triple1) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Bob is not cold.
Unknown
inv-rconc
[@1: Bob is cold.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "cold" "-")
Erin is young.
Unknown
rconc
[@1: Erin is young.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "young" "+")
Bob is not smart.
Unknown
inv-rconc
[@2: Bob is smart.[CWA. Example of deepest failure = (rule5 <- rule1 <- FAIL)]]
("Bob" "is" "smart" "-")
Fiona is quiet.
Unknown
rconc
[@1: Fiona is quiet.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Fiona" "is" "quiet" "+")
Bob is not big.
Unknown
inv-random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "-")
Fiona is big.
Unknown
random
[@0: Fiona is big.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "big" "+")
@0: Anne is big.[(triple1)] Anne is furry.[(triple2)] Anne is quiet.[(triple3 OR ((triple1 triple2) -> rule2))] Bob is furry.[(triple4)] Bob is nice.[(triple5)] Bob is quiet.[(triple6)] Erin is cold.[(triple8)] Erin is furry.[(triple9)] Erin is not big.[(triple7)] Erin is quiet.[(triple10)] Erin is smart.[(triple11)] Fiona is cold.[(triple12)] Fiona is furry.[(triple13)] Fiona is nice.[(triple14)] Fiona is not young.[(triple15)] @1: Anne is young.[(((triple1) -> rule1))] Erin is nice.[(((triple11 triple7) -> rule4))] @2: Anne is smart.[(((((triple1) -> rule1)) -> rule5))] @3: Anne is cold.[(((triple1 ((((triple1) -> rule1)) -> rule5)) -> rule3))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is furry.
("Anne" "is" "furry" "+")
triple2
Anne is quiet.
("Anne" "is" "quiet" "+")
triple3
((triple1 triple2) -> (rule2 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
triple4
Bob is nice.
("Bob" "is" "nice" "+")
triple5
Bob is quiet.
("Bob" "is" "quiet" "+")
triple6
Erin is cold.
("Erin" "is" "cold" "+")
triple8
Erin is furry.
("Erin" "is" "furry" "+")
triple9
Erin is not big.
("Erin" "is" "big" "-")
triple7
Erin is quiet.
("Erin" "is" "quiet" "+")
triple10
Erin is smart.
("Erin" "is" "smart" "+")
triple11
Fiona is cold.
("Fiona" "is" "cold" "+")
triple12
Fiona is furry.
("Fiona" "is" "furry" "+")
triple13
Fiona is nice.
("Fiona" "is" "nice" "+")
triple14
Fiona is not young.
("Fiona" "is" "young" "-")
triple15
Anne is young.
("Anne" "is" "young" "+")
((triple1) -> (rule1 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
((triple11 triple7) -> (rule4 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
((((triple1) -> (rule1 % int2))) -> (rule5 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
((triple1 ((((triple1) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3