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