Anne is green. Anne is white. Charlie is green. Charlie is kind. Charlie is white. Charlie is young. Gary is kind. Harry is green. Harry is nice. Harry is white. Harry is young. If something is smart then it is young. All nice, smart things are round. Smart things are green. Young, round things are white. Round, nice things are smart. If Gary is kind then Gary is green. Kind things are round. All round things are nice.
Anne is green.
("Anne" "is" "green" "+")
Anne is white.
("Anne" "is" "white" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is white.
("Harry" "is" "white" "+")
Harry is young.
("Harry" "is" "young" "+")
If something is smart then it is young.
((("something" "is" "smart" "+")) -> ("something" "is" "young" "+"))
All nice, smart things are round.
((("something" "is" "nice" "+") ("something" "is" "smart" "+")) -> ("something" "is" "round" "+"))
Smart things are green.
((("something" "is" "smart" "+")) -> ("something" "is" "green" "+"))
Young, round things are white.
((("something" "is" "young" "+") ("something" "is" "round" "+")) -> ("something" "is" "white" "+"))
Round, nice things are smart.
((("something" "is" "round" "+") ("something" "is" "nice" "+")) -> ("something" "is" "smart" "+"))
If Gary is kind then Gary is green.
((("Gary" "is" "kind" "+")) -> ("Gary" "is" "green" "+"))
Kind things are round.
((("something" "is" "kind" "+")) -> ("something" "is" "round" "+"))
All round things are nice.
((("something" "is" "round" "+")) -> ("something" "is" "nice" "+"))
Gary is kind.
True
1
proof
[(triple7)]
("Gary" "is" "kind" "+")
triple7
Charlie is not white.
False
1
inv-proof
[(triple5 OR ((triple6 ((triple4) -> rule7)) -> rule4) OR ((((((((triple4) -> rule7) ((((triple4) -> rule7)) -> rule8)) -> rule5)) -> rule1) ((triple4) -> rule7)) -> rule4))]
("Charlie" "is" "white" "-")
triple5
((triple6 ((triple4) -> (rule7 % int2))) -> (rule4 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
((((((((triple4) -> (rule7 % int5)) ((((triple4) -> (rule7 % int5))) -> (rule8 % int4))) -> (rule5 % int3))) -> (rule1 % int2)) ((triple4) -> (rule7 % int5))) -> (rule4 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
Charlie is nice.
("Charlie" "is" "nice" "+")
int4
Charlie is round.
("Charlie" "is" "round" "+")
int5
Gary is green.
True
2
proof
[(((triple7) -> rule6) OR ((((((triple7) -> rule7) ((((triple7) -> rule7)) -> rule8)) -> rule5)) -> rule3))]
("Gary" "is" "green" "+")
((triple7) -> (rule6 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
((((((triple7) -> (rule7 % int4)) ((((triple7) -> (rule7 % int4))) -> (rule8 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
Gary is round.
("Gary" "is" "round" "+")
int4
Charlie is not round.
False
2
inv-proof
[(((triple4) -> rule7))]
("Charlie" "is" "round" "-")
((triple4) -> (rule7 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is nice.
True
3
proof
[(((((triple4) -> rule7)) -> rule8))]
("Charlie" "is" "nice" "+")
((((triple4) -> (rule7 % int2))) -> (rule8 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Gary is not nice.
False
3
inv-proof
[(((((triple7) -> rule7)) -> rule8))]
("Gary" "is" "nice" "-")
((((triple7) -> (rule7 % int2))) -> (rule8 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Charlie is smart.
True
6
proof
[(((((triple4) -> rule7) ((((triple4) -> rule7)) -> rule8)) -> rule5))]
("Charlie" "is" "smart" "+")
((((triple4) -> (rule7 % int3)) ((((triple4) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
Gary is not smart.
False
6
inv-proof
[(((((triple7) -> rule7) ((((triple7) -> rule7)) -> rule8)) -> rule5))]
("Gary" "is" "smart" "-")
((((triple7) -> (rule7 % int3)) ((((triple7) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
Gary is young.
True
7
proof
[(((((((triple7) -> rule7) ((((triple7) -> rule7)) -> rule8)) -> rule5)) -> rule1))]
("Gary" "is" "young" "+")
((((((triple7) -> (rule7 % int4)) ((((triple7) -> (rule7 % int4))) -> (rule8 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
Gary is round.
("Gary" "is" "round" "+")
int4
Gary is not young.
False
7
inv-proof
[(((((((triple7) -> rule7) ((((triple7) -> rule7)) -> rule8)) -> rule5)) -> rule1))]
("Gary" "is" "young" "-")
((((((triple7) -> (rule7 % int4)) ((((triple7) -> (rule7 % int4))) -> (rule8 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
Gary is round.
("Gary" "is" "round" "+")
int4
Gary is white.
True
10
proof
[(((((((((triple7) -> rule7) ((((triple7) -> rule7)) -> rule8)) -> rule5)) -> rule1) ((triple7) -> rule7)) -> rule4))]
("Gary" "is" "white" "+")
((((((((triple7) -> (rule7 % int5)) ((((triple7) -> (rule7 % int5))) -> (rule8 % int4))) -> (rule5 % int3))) -> (rule1 % int2)) ((triple7) -> (rule7 % int5))) -> (rule4 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Gary is nice.
("Gary" "is" "nice" "+")
int4
Gary is round.
("Gary" "is" "round" "+")
int5
Gary is not white.
False
10
inv-proof
[(((((((((triple7) -> rule7) ((((triple7) -> rule7)) -> rule8)) -> rule5)) -> rule1) ((triple7) -> rule7)) -> rule4))]
("Gary" "is" "white" "-")
((((((((triple7) -> (rule7 % int5)) ((((triple7) -> (rule7 % int5))) -> (rule8 % int4))) -> (rule5 % int3))) -> (rule1 % int2)) ((triple7) -> (rule7 % int5))) -> (rule4 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Gary is nice.
("Gary" "is" "nice" "+")
int4
Gary is round.
("Gary" "is" "round" "+")
int5
Harry is not smart.
Unknown
inv-rconc
[@2: Harry is smart.[CWA. Example of deepest failure = (rule5 <- rule2 <- FAIL)]]
("Harry" "is" "smart" "-")
Anne is smart.
Unknown
rconc
[@2: Anne is smart.[CWA. Example of deepest failure = (rule5 <- rule2 <- FAIL)]]
("Anne" "is" "smart" "+")
Anne is not nice.
Unknown
inv-rconc
[@2: Anne is nice.[CWA. Example of deepest failure = (rule8 <- rule2 <- FAIL)]]
("Anne" "is" "nice" "-")
Anne is young.
Unknown
rconc
[@3: Anne is young.[CWA. Example of deepest failure = (rule1 <- rule5 <- rule2 <- FAIL)]]
("Anne" "is" "young" "+")
Anne is not round.
Unknown
inv-rconc
[@3: Anne is round.[CWA. Example of deepest failure = (rule2 <- rule8 <- rule7 <- FAIL)]]
("Anne" "is" "round" "-")
Harry is round.
Unknown
rconc
[@3: Harry is round.[CWA. Example of deepest failure = (rule2 <- rule5 <- rule7 <- FAIL)]]
("Harry" "is" "round" "+")
Anne is not kind.
Unknown
inv-random
[@0: Anne is kind.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "kind" "-")
Harry is kind.
Unknown
random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "+")
@0: Anne is green.[(triple1)] Anne is white.[(triple2)] Charlie is green.[(triple3 OR ((((((triple4) -> rule7) ((((triple4) -> rule7)) -> rule8)) -> rule5)) -> rule3))] Charlie is kind.[(triple4)] Charlie is white.[(triple5 OR ((triple6 ((triple4) -> rule7)) -> rule4) OR ((((((((triple4) -> rule7) ((((triple4) -> rule7)) -> rule8)) -> rule5)) -> rule1) ((triple4) -> rule7)) -> rule4))] Charlie is young.[(triple6 OR ((((((triple4) -> rule7) ((((triple4) -> rule7)) -> rule8)) -> rule5)) -> rule1))] Gary is kind.[(triple7)] Harry is green.[(triple8)] Harry is nice.[(triple9)] Harry is white.[(triple10)] Harry is young.[(triple11)] @1: Charlie is round.[(((triple4) -> rule7))] Gary is green.[(((triple7) -> rule6) OR ((((((triple7) -> rule7) ((((triple7) -> rule7)) -> rule8)) -> rule5)) -> rule3))] Gary is round.[(((triple7) -> rule7))] @2: Charlie is nice.[(((((triple4) -> rule7)) -> rule8))] Gary is nice.[(((((triple7) -> rule7)) -> rule8))] @3: Charlie is smart.[(((((triple4) -> rule7) ((((triple4) -> rule7)) -> rule8)) -> rule5))] Gary is smart.[(((((triple7) -> rule7) ((((triple7) -> rule7)) -> rule8)) -> rule5))] @4: Gary is young.[(((((((triple7) -> rule7) ((((triple7) -> rule7)) -> rule8)) -> rule5)) -> rule1))] @5: Gary is white.[(((((((((triple7) -> rule7) ((((triple7) -> rule7)) -> rule8)) -> rule5)) -> rule1) ((triple7) -> rule7)) -> rule4))]
Anne is green.
("Anne" "is" "green" "+")
triple1
Anne is white.
("Anne" "is" "white" "+")
triple2
Charlie is green.
("Charlie" "is" "green" "+")
triple3
((((((triple4) -> (rule7 % int4)) ((((triple4) -> (rule7 % int4))) -> (rule8 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Charlie is round.
("Charlie" "is" "round" "+")
int4
Charlie is kind.
("Charlie" "is" "kind" "+")
triple4
Charlie is white.
("Charlie" "is" "white" "+")
triple5
((triple6 ((triple4) -> (rule7 % int2))) -> (rule4 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
((((((((triple4) -> (rule7 % int5)) ((((triple4) -> (rule7 % int5))) -> (rule8 % int4))) -> (rule5 % int3))) -> (rule1 % int2)) ((triple4) -> (rule7 % int5))) -> (rule4 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
Charlie is nice.
("Charlie" "is" "nice" "+")
int4
Charlie is round.
("Charlie" "is" "round" "+")
int5
Charlie is young.
("Charlie" "is" "young" "+")
triple6
((((((triple4) -> (rule7 % int4)) ((((triple4) -> (rule7 % int4))) -> (rule8 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Charlie is round.
("Charlie" "is" "round" "+")
int4
Gary is kind.
("Gary" "is" "kind" "+")
triple7
Harry is green.
("Harry" "is" "green" "+")
triple8
Harry is nice.
("Harry" "is" "nice" "+")
triple9
Harry is white.
("Harry" "is" "white" "+")
triple10
Harry is young.
("Harry" "is" "young" "+")
triple11
Charlie is round.
("Charlie" "is" "round" "+")
((triple4) -> (rule7 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
((triple7) -> (rule6 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
((((((triple7) -> (rule7 % int4)) ((((triple7) -> (rule7 % int4))) -> (rule8 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
Gary is round.
("Gary" "is" "round" "+")
int4
Gary is round.
("Gary" "is" "round" "+")
((triple7) -> (rule7 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
((((triple4) -> (rule7 % int2))) -> (rule8 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
((((triple7) -> (rule7 % int2))) -> (rule8 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
((((triple4) -> (rule7 % int3)) ((((triple4) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
Gary is smart.
("Gary" "is" "smart" "+")
((((triple7) -> (rule7 % int3)) ((((triple7) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
Gary is young.
("Gary" "is" "young" "+")
((((((triple7) -> (rule7 % int4)) ((((triple7) -> (rule7 % int4))) -> (rule8 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
Gary is round.
("Gary" "is" "round" "+")
int4
Gary is white.
("Gary" "is" "white" "+")
((((((((triple7) -> (rule7 % int5)) ((((triple7) -> (rule7 % int5))) -> (rule8 % int4))) -> (rule5 % int3))) -> (rule1 % int2)) ((triple7) -> (rule7 % int5))) -> (rule4 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Gary is nice.
("Gary" "is" "nice" "+")
int4
Gary is round.
("Gary" "is" "round" "+")
int5