Anne is cold. Anne is nice. Anne is quiet. Bob is big. Bob is cold. Bob is nice. Bob is quiet. Harry is big. Harry is furry. Harry is nice. All nice things are smart. All kind things are furry. All quiet things are furry. If something is kind then it is furry. All furry, quiet things are cold. If something is smart and cold then it is quiet. All cold things are big. Quiet, kind things are cold.
Anne is cold.
("Anne" "is" "cold" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Bob is big.
("Bob" "is" "big" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is nice.
("Harry" "is" "nice" "+")
All nice things are smart.
((("something" "is" "nice" "+")) -> ("something" "is" "smart" "+"))
All kind things are furry.
((("something" "is" "kind" "+")) -> ("something" "is" "furry" "+"))
All quiet things are furry.
((("something" "is" "quiet" "+")) -> ("something" "is" "furry" "+"))
If something is kind then it is furry.
((("something" "is" "kind" "+")) -> ("something" "is" "furry" "+"))
All furry, quiet things are cold.
((("something" "is" "furry" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "cold" "+"))
If something is smart and cold then it is quiet.
((("something" "is" "smart" "+") ("something" "is" "cold" "+")) -> ("something" "is" "quiet" "+"))
All cold things are big.
((("something" "is" "cold" "+")) -> ("something" "is" "big" "+"))
Quiet, kind things are cold.
((("something" "is" "quiet" "+") ("something" "is" "kind" "+")) -> ("something" "is" "cold" "+"))
Harry is nice.
True
1
proof
[(triple10)]
("Harry" "is" "nice" "+")
triple10
Anne is not nice.
False
1
inv-proof
[(triple2)]
("Anne" "is" "nice" "-")
triple2
Harry is not quiet.
Unknown
inv-rconc
[@2: Harry is quiet.[CWA. Example of deepest failure = (rule6 <- rule5 <- FAIL)]]
("Harry" "is" "quiet" "-")
Harry is kind.
Unknown
random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "+")
@0: Anne is cold.[(triple1 OR ((((triple3) -> rule3) triple3) -> rule5))] Anne is nice.[(triple2)] Anne is quiet.[(triple3 OR ((((triple2) -> rule1) triple1) -> rule6))] Bob is big.[(triple4 OR ((triple5) -> rule7) OR ((((((triple7) -> rule3) triple7) -> rule5)) -> rule7))] Bob is cold.[(triple5 OR ((((triple7) -> rule3) triple7) -> rule5))] Bob is nice.[(triple6)] Bob is quiet.[(triple7 OR ((((triple6) -> rule1) triple5) -> rule6))] Harry is big.[(triple8)] Harry is furry.[(triple9)] Harry is nice.[(triple10)] @1: Anne is big.[(((triple1) -> rule7) OR ((((((triple3) -> rule3) triple3) -> rule5)) -> rule7))] Anne is furry.[(((triple3) -> rule3) OR ((((((triple2) -> rule1) triple1) -> rule6)) -> rule3))] Anne is smart.[(((triple2) -> rule1))] Bob is furry.[(((triple7) -> rule3) OR ((((((triple6) -> rule1) triple5) -> rule6)) -> rule3))] Bob is smart.[(((triple6) -> rule1))] Harry is smart.[(((triple10) -> rule1))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
((((triple3) -> (rule3 % int2)) triple3) -> (rule5 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
triple2
Anne is quiet.
("Anne" "is" "quiet" "+")
triple3
((((triple2) -> (rule1 % int2)) triple1) -> (rule6 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
triple4
((triple5) -> (rule7 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
((((((triple7) -> (rule3 % int3)) triple7) -> (rule5 % int2))) -> (rule7 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
Bob is cold.
("Bob" "is" "cold" "+")
triple5
((((triple7) -> (rule3 % int2)) triple7) -> (rule5 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
triple6
Bob is quiet.
("Bob" "is" "quiet" "+")
triple7
((((triple6) -> (rule1 % int2)) triple5) -> (rule6 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
triple8
Harry is furry.
("Harry" "is" "furry" "+")
triple9
Harry is nice.
("Harry" "is" "nice" "+")
triple10
Anne is big.
("Anne" "is" "big" "+")
((triple1) -> (rule7 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
((((((triple3) -> (rule3 % int3)) triple3) -> (rule5 % int2))) -> (rule7 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Anne is furry.
("Anne" "is" "furry" "+")
((triple3) -> (rule3 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
((((((triple2) -> (rule1 % int3)) triple1) -> (rule6 % int2))) -> (rule3 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Anne is smart.
("Anne" "is" "smart" "+")
((triple2) -> (rule1 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
((triple7) -> (rule3 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
((((((triple6) -> (rule1 % int3)) triple5) -> (rule6 % int2))) -> (rule3 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Bob is smart.
("Bob" "is" "smart" "+")
((triple6) -> (rule1 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
((triple10) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1