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