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