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