Anne is big. Anne is rough. Dave is not kind. Erin is white. Harry is kind. Harry is not quiet. Harry is not rough. If Anne is white and Anne is kind then Anne is round. White, round things are rough. All kind, nice things are rough. Nice things are round. All white things are nice. If something is white and rough then it is kind. If Dave is rough and Dave is big then Dave is quiet. If something is rough and kind then it is big. If something is quiet and not round then it is big.
Anne is big.
("Anne" "is" "big" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Dave is not kind.
("Dave" "is" "kind" "-")
Erin is white.
("Erin" "is" "white" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is not quiet.
("Harry" "is" "quiet" "-")
Harry is not rough.
("Harry" "is" "rough" "-")
If Anne is white and Anne is kind then Anne is round.
((("Anne" "is" "white" "+") ("Anne" "is" "kind" "+")) -> ("Anne" "is" "round" "+"))
White, round things are rough.
((("something" "is" "white" "+") ("something" "is" "round" "+")) -> ("something" "is" "rough" "+"))
All kind, nice things are rough.
((("something" "is" "kind" "+") ("something" "is" "nice" "+")) -> ("something" "is" "rough" "+"))
Nice things are round.
((("something" "is" "nice" "+")) -> ("something" "is" "round" "+"))
All white things are nice.
((("something" "is" "white" "+")) -> ("something" "is" "nice" "+"))
If something is white and rough then it is kind.
((("something" "is" "white" "+") ("something" "is" "rough" "+")) -> ("something" "is" "kind" "+"))
If Dave is rough and Dave is big then Dave is quiet.
((("Dave" "is" "rough" "+") ("Dave" "is" "big" "+")) -> ("Dave" "is" "quiet" "+"))
If something is rough and kind then it is big.
((("something" "is" "rough" "+") ("something" "is" "kind" "+")) -> ("something" "is" "big" "+"))
If something is quiet and not round then it is big.
((("something" "is" "quiet" "+") ("something" "is" "round" "~")) -> ("something" "is" "big" "+"))
Dave is not kind.
True
1
proof
[(triple3)]
("Dave" "is" "kind" "-")
triple3
Anne is not big.
False
1
inv-proof
[(triple1)]
("Anne" "is" "big" "-")
triple1
Erin is nice.
True
2
proof
[(((triple4) -> rule5))]
("Erin" "is" "nice" "+")
((triple4) -> (rule5 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is not nice.
False
2
inv-proof
[(((triple4) -> rule5))]
("Erin" "is" "nice" "-")
((triple4) -> (rule5 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is round.
True
3
proof
[(((((triple4) -> rule5)) -> rule4))]
("Erin" "is" "round" "+")
((((triple4) -> (rule5 % int2))) -> (rule4 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is not round.
False
3
inv-proof
[(((((triple4) -> rule5)) -> rule4))]
("Erin" "is" "round" "-")
((((triple4) -> (rule5 % int2))) -> (rule4 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is rough.
True
5
proof
[(((triple4 ((((triple4) -> rule5)) -> rule4)) -> rule2))]
("Erin" "is" "rough" "+")
((triple4 ((((triple4) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
int3
Erin is not rough.
False
5
inv-proof
[(((triple4 ((((triple4) -> rule5)) -> rule4)) -> rule2))]
("Erin" "is" "rough" "-")
((triple4 ((((triple4) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
int3
Erin is kind.
True
7
proof
[(((triple4 ((triple4 ((((triple4) -> rule5)) -> rule4)) -> rule2)) -> rule6))]
("Erin" "is" "kind" "+")
((triple4 ((triple4 ((((triple4) -> (rule5 % int4))) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
Erin is nice.
("Erin" "is" "nice" "+")
int4
Erin is not kind.
False
7
inv-proof
[(((triple4 ((triple4 ((((triple4) -> rule5)) -> rule4)) -> rule2)) -> rule6))]
("Erin" "is" "kind" "-")
((triple4 ((triple4 ((((triple4) -> (rule5 % int4))) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
Erin is nice.
("Erin" "is" "nice" "+")
int4
Erin is big.
True
13
proof
[(((((triple4 ((((triple4) -> rule5)) -> rule4)) -> rule2) ((triple4 ((triple4 ((((triple4) -> rule5)) -> rule4)) -> rule2)) -> rule6)) -> rule8))]
("Erin" "is" "big" "+")
((((triple4 ((((triple4) -> (rule5 % int5))) -> (rule4 % int4))) -> (rule2 % int3)) ((triple4 ((triple4 ((((triple4) -> (rule5 % int5))) -> (rule4 % int4))) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
Erin is round.
("Erin" "is" "round" "+")
int4
Erin is nice.
("Erin" "is" "nice" "+")
int5
Erin is not big.
False
13
inv-proof
[(((((triple4 ((((triple4) -> rule5)) -> rule4)) -> rule2) ((triple4 ((triple4 ((((triple4) -> rule5)) -> rule4)) -> rule2)) -> rule6)) -> rule8))]
("Erin" "is" "big" "-")
((((triple4 ((((triple4) -> (rule5 % int5))) -> (rule4 % int4))) -> (rule2 % int3)) ((triple4 ((triple4 ((((triple4) -> (rule5 % int5))) -> (rule4 % int4))) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
Erin is round.
("Erin" "is" "round" "+")
int4
Erin is nice.
("Erin" "is" "nice" "+")
int5
Anne is not kind.
Unknown
inv-rconc
[@1: Anne is kind.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Anne" "is" "kind" "-")
Anne is round.
Unknown
rconc
[@2: Anne is round.[CWA. Example of deepest failure = (rule4 <- rule5 <- FAIL)]]
("Anne" "is" "round" "+")
Anne is not nice.
Unknown
inv-rconc
[@1: Anne is nice.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Anne" "is" "nice" "-")
Dave is big.
Unknown
rconc
[@1: Dave is big.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Dave" "is" "big" "+")
Dave is not nice.
Unknown
inv-rconc
[@1: Dave is nice.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Dave" "is" "nice" "-")
Harry is nice.
Unknown
rconc
[@1: Harry is nice.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Harry" "is" "nice" "+")
Dave is not white.
Unknown
inv-random
[@0: Dave is white.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "white" "-")
Anne is quiet.
Unknown
random
[@0: Anne is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "quiet" "+")
Erin is not quiet.
Unknown
inv-random
[@0: Erin is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "quiet" "-")
Harry is white.
Unknown
random
[@0: Harry is white.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "white" "+")
@0: Anne is big.[(triple1)] Anne is rough.[(triple2)] Dave is not kind.[(triple3)] Erin is white.[(triple4)] Harry is kind.[(triple5)] Harry is not quiet.[(triple6)] Harry is not rough.[(triple7)] @1: Erin is nice.[(((triple4) -> rule5))] @2: Erin is round.[(((((triple4) -> rule5)) -> rule4))] @3: Erin is rough.[(((triple4 ((((triple4) -> rule5)) -> rule4)) -> rule2))] @4: Erin is kind.[(((triple4 ((triple4 ((((triple4) -> rule5)) -> rule4)) -> rule2)) -> rule6))] @5: Erin is big.[(((((triple4 ((((triple4) -> rule5)) -> rule4)) -> rule2) ((triple4 ((triple4 ((((triple4) -> rule5)) -> rule4)) -> rule2)) -> rule6)) -> rule8))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is rough.
("Anne" "is" "rough" "+")
triple2
Dave is not kind.
("Dave" "is" "kind" "-")
triple3
Erin is white.
("Erin" "is" "white" "+")
triple4
Harry is kind.
("Harry" "is" "kind" "+")
triple5
Harry is not quiet.
("Harry" "is" "quiet" "-")
triple6
Harry is not rough.
("Harry" "is" "rough" "-")
triple7
Erin is nice.
("Erin" "is" "nice" "+")
((triple4) -> (rule5 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
((((triple4) -> (rule5 % int2))) -> (rule4 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
((triple4 ((((triple4) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
int3
Erin is kind.
("Erin" "is" "kind" "+")
((triple4 ((triple4 ((((triple4) -> (rule5 % int4))) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
Erin is nice.
("Erin" "is" "nice" "+")
int4
Erin is big.
("Erin" "is" "big" "+")
((((triple4 ((((triple4) -> (rule5 % int5))) -> (rule4 % int4))) -> (rule2 % int3)) ((triple4 ((triple4 ((((triple4) -> (rule5 % int5))) -> (rule4 % int4))) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
Erin is round.
("Erin" "is" "round" "+")
int4
Erin is nice.
("Erin" "is" "nice" "+")
int5