Anne is quiet. Anne is white. Charlie is big. Charlie is cold. Charlie is nice. Charlie is smart. Charlie is white. Dave is big. Dave is cold. Dave is nice. Dave is quiet. Harry is big. Harry is kind. Harry is quiet. Harry is white. All kind things are nice. If something is nice and big then it is kind. If Charlie is kind then Charlie is quiet. Nice things are quiet. All white, nice things are smart. White things are kind. Quiet, cold things are nice. If something is kind and smart then it is cold.
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is white.
("Anne" "is" "white" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is white.
("Harry" "is" "white" "+")
All kind things are nice.
((("something" "is" "kind" "+")) -> ("something" "is" "nice" "+"))
If something is nice and big then it is kind.
((("something" "is" "nice" "+") ("something" "is" "big" "+")) -> ("something" "is" "kind" "+"))
If Charlie is kind then Charlie is quiet.
((("Charlie" "is" "kind" "+")) -> ("Charlie" "is" "quiet" "+"))
Nice things are quiet.
((("something" "is" "nice" "+")) -> ("something" "is" "quiet" "+"))
All white, nice things are smart.
((("something" "is" "white" "+") ("something" "is" "nice" "+")) -> ("something" "is" "smart" "+"))
White things are kind.
((("something" "is" "white" "+")) -> ("something" "is" "kind" "+"))
Quiet, cold things are nice.
((("something" "is" "quiet" "+") ("something" "is" "cold" "+")) -> ("something" "is" "nice" "+"))
If something is kind and smart then it is cold.
((("something" "is" "kind" "+") ("something" "is" "smart" "+")) -> ("something" "is" "cold" "+"))
Harry is big.
True
1
proof
[(triple12)]
("Harry" "is" "big" "+")
triple12
Harry is not white.
False
1
inv-proof
[(triple15)]
("Harry" "is" "white" "-")
triple15
Harry is nice.
True
2
proof
[(((triple13) -> rule1) OR ((((triple15) -> rule6)) -> rule1))]
("Harry" "is" "nice" "+")
((triple13) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
((((triple15) -> (rule6 % int2))) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Dave is not kind.
False
3
inv-proof
[(((triple10 triple8) -> rule2) OR ((((triple11 triple9) -> rule7) triple8) -> rule2))]
("Dave" "is" "kind" "-")
((triple10 triple8) -> (rule2 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
((((triple11 triple9) -> (rule7 % int2)) triple8) -> (rule2 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Anne is nice.
True
3
proof
[(((((triple2) -> rule6)) -> rule1))]
("Anne" "is" "nice" "+")
((((triple2) -> (rule6 % int2))) -> (rule1 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Harry is not smart.
False
4
inv-proof
[(((triple15 ((triple13) -> rule1)) -> rule5) OR ((triple15 ((((triple15) -> rule6)) -> rule1)) -> rule5))]
("Harry" "is" "smart" "-")
((triple15 ((triple13) -> (rule1 % int2))) -> (rule5 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
((triple15 ((((triple15) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
Dave is not smart.
Unknown
inv-rconc
[@1: Dave is smart.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Dave" "is" "smart" "-")
Dave is white.
Unknown
random
[@0: Dave is white.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "white" "+")
@0: Anne is quiet.[(triple1 OR ((((((triple2) -> rule6)) -> rule1)) -> rule4))] Anne is white.[(triple2)] Charlie is big.[(triple3)] Charlie is cold.[(triple4 OR ((((triple7) -> rule6) triple6) -> rule8) OR ((((triple5 triple3) -> rule2) triple6) -> rule8) OR ((((triple7) -> rule6) ((triple7 triple5) -> rule5)) -> rule8) OR ((((triple5 triple3) -> rule2) ((triple7 triple5) -> rule5)) -> rule8) OR ((((triple7) -> rule6) ((triple7 ((((triple7) -> rule6)) -> rule1)) -> rule5)) -> rule8) OR ((((triple5 triple3) -> rule2) ((triple7 ((((triple7) -> rule6)) -> rule1)) -> rule5)) -> rule8))] Charlie is nice.[(triple5 OR ((((triple7) -> rule6)) -> rule1) OR ((((((triple7) -> rule6)) -> rule3) triple4) -> rule7) OR ((((((triple7) -> rule6)) -> rule3) ((((triple7) -> rule6) triple6) -> rule8)) -> rule7))] Charlie is smart.[(triple6 OR ((triple7 triple5) -> rule5) OR ((triple7 ((((triple7) -> rule6)) -> rule1)) -> rule5) OR ((triple7 ((((((triple7) -> rule6)) -> rule3) triple4) -> rule7)) -> rule5))] Charlie is white.[(triple7)] Dave is big.[(triple8)] Dave is cold.[(triple9)] Dave is nice.[(triple10 OR ((triple11 triple9) -> rule7))] Dave is quiet.[(triple11 OR ((triple10) -> rule4))] Harry is big.[(triple12)] Harry is kind.[(triple13 OR ((triple15) -> rule6))] Harry is quiet.[(triple14 OR ((((triple13) -> rule1)) -> rule4) OR ((((((triple15) -> rule6)) -> rule1)) -> rule4))] Harry is white.[(triple15)] @1: Anne is kind.[(((triple2) -> rule6))] Charlie is kind.[(((triple7) -> rule6) OR ((triple5 triple3) -> rule2))] Charlie is quiet.[(((triple5) -> rule4) OR ((((triple7) -> rule6)) -> rule3) OR ((((triple5 triple3) -> rule2)) -> rule3) OR ((((((triple7) -> rule6)) -> rule1)) -> rule4))] Dave is kind.[(((triple10 triple8) -> rule2) OR ((((triple11 triple9) -> rule7) triple8) -> rule2))] Harry is nice.[(((triple13) -> rule1) OR ((((triple15) -> rule6)) -> rule1))] @2: Anne is nice.[(((((triple2) -> rule6)) -> rule1))] Harry is smart.[(((triple15 ((triple13) -> rule1)) -> rule5) OR ((triple15 ((((triple15) -> rule6)) -> rule1)) -> rule5))] @3: Anne is smart.[(((triple2 ((((triple2) -> rule6)) -> rule1)) -> rule5))] Harry is cold.[(((triple13 ((triple15 ((triple13) -> rule1)) -> rule5)) -> rule8) OR ((((triple15) -> rule6) ((triple15 ((triple13) -> rule1)) -> rule5)) -> rule8) OR ((triple13 ((triple15 ((((triple15) -> rule6)) -> rule1)) -> rule5)) -> rule8) OR ((((triple15) -> rule6) ((triple15 ((((triple15) -> rule6)) -> rule1)) -> rule5)) -> rule8))] @4: Anne is cold.[(((((triple2) -> rule6) ((triple2 ((((triple2) -> rule6)) -> rule1)) -> rule5)) -> rule8))]
Anne is quiet.
("Anne" "is" "quiet" "+")
triple1
((((((triple2) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
Anne is white.
("Anne" "is" "white" "+")
triple2
Charlie is big.
("Charlie" "is" "big" "+")
triple3
Charlie is cold.
("Charlie" "is" "cold" "+")
triple4
((((triple7) -> (rule6 % int2)) triple6) -> (rule8 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
((((triple5 triple3) -> (rule2 % int2)) triple6) -> (rule8 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
((((triple7) -> (rule6 % int3)) ((triple7 triple5) -> (rule5 % int2))) -> (rule8 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
((((triple5 triple3) -> (rule2 % int3)) ((triple7 triple5) -> (rule5 % int2))) -> (rule8 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
((((triple7) -> (rule6 % int4)) ((triple7 ((((triple7) -> (rule6 % int4))) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Charlie is kind.
("Charlie" "is" "kind" "+")
int4
((((triple5 triple3) -> (rule2 % int4)) ((triple7 ((((triple7) -> (rule6 % int4))) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Charlie is kind.
("Charlie" "is" "kind" "+")
int4
Charlie is nice.
("Charlie" "is" "nice" "+")
triple5
((((triple7) -> (rule6 % int2))) -> (rule1 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
((((((triple7) -> (rule6 % int3))) -> (rule3 % int2)) triple4) -> (rule7 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
((((((triple7) -> (rule6 % int4))) -> (rule3 % int3)) ((((triple7) -> (rule6 % int4)) triple6) -> (rule8 % int2))) -> (rule7 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
Charlie is kind.
("Charlie" "is" "kind" "+")
int4
Charlie is smart.
("Charlie" "is" "smart" "+")
triple6
((triple7 triple5) -> (rule5 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
((triple7 ((((triple7) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
((triple7 ((((((triple7) -> (rule6 % int4))) -> (rule3 % int3)) triple4) -> (rule7 % int2))) -> (rule5 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
Charlie is kind.
("Charlie" "is" "kind" "+")
int4
Charlie is white.
("Charlie" "is" "white" "+")
triple7
Dave is big.
("Dave" "is" "big" "+")
triple8
Dave is cold.
("Dave" "is" "cold" "+")
triple9
Dave is nice.
("Dave" "is" "nice" "+")
triple10
((triple11 triple9) -> (rule7 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
triple11
((triple10) -> (rule4 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
triple12
Harry is kind.
("Harry" "is" "kind" "+")
triple13
((triple15) -> (rule6 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
triple14
((((triple13) -> (rule1 % int2))) -> (rule4 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
((((((triple15) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
Harry is white.
("Harry" "is" "white" "+")
triple15
Anne is kind.
("Anne" "is" "kind" "+")
((triple2) -> (rule6 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
((triple7) -> (rule6 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
((triple5 triple3) -> (rule2 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((triple5) -> (rule4 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
((((triple7) -> (rule6 % int2))) -> (rule3 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
((((triple5 triple3) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
((((((triple7) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Dave is kind.
("Dave" "is" "kind" "+")
((triple10 triple8) -> (rule2 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
((((triple11 triple9) -> (rule7 % int2)) triple8) -> (rule2 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
((triple13) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
((((triple15) -> (rule6 % int2))) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
((((triple2) -> (rule6 % int2))) -> (rule1 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
((triple15 ((triple13) -> (rule1 % int2))) -> (rule5 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
((triple15 ((((triple15) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
Anne is smart.
("Anne" "is" "smart" "+")
((triple2 ((((triple2) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
Harry is cold.
("Harry" "is" "cold" "+")
((triple13 ((triple15 ((triple13) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
((((triple15) -> (rule6 % int4)) ((triple15 ((triple13) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Harry is kind.
("Harry" "is" "kind" "+")
int4
((triple13 ((triple15 ((((triple15) -> (rule6 % int4))) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Harry is kind.
("Harry" "is" "kind" "+")
int4
((((triple15) -> (rule6 % int4)) ((triple15 ((((triple15) -> (rule6 % int4))) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Harry is kind.
("Harry" "is" "kind" "+")
int4
Anne is cold.
("Anne" "is" "cold" "+")
((((triple2) -> (rule6 % int4)) ((triple2 ((((triple2) -> (rule6 % int4))) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Anne is kind.
("Anne" "is" "kind" "+")
int4