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