Charlie is kind. Charlie is quiet. Erin is kind. Erin is white. Fiona is quiet. Fiona is rough. Fiona is young. Gary is blue. Gary is kind. Gary is rough. Gary is young. If Gary is quiet and Gary is rough then Gary is white. Furry, rough things are white. All kind, quiet things are furry. Blue things are rough. White, furry things are kind. Blue things are furry. If something is white then it is young. If Erin is white then Erin is kind. All furry things are blue.
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is white.
("Erin" "is" "white" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Fiona is young.
("Fiona" "is" "young" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is young.
("Gary" "is" "young" "+")
If Gary is quiet and Gary is rough then Gary is white.
((("Gary" "is" "quiet" "+") ("Gary" "is" "rough" "+")) -> ("Gary" "is" "white" "+"))
Furry, rough things are white.
((("something" "is" "furry" "+") ("something" "is" "rough" "+")) -> ("something" "is" "white" "+"))
All kind, quiet things are furry.
((("something" "is" "kind" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "furry" "+"))
Blue things are rough.
((("something" "is" "blue" "+")) -> ("something" "is" "rough" "+"))
White, furry things are kind.
((("something" "is" "white" "+") ("something" "is" "furry" "+")) -> ("something" "is" "kind" "+"))
Blue things are furry.
((("something" "is" "blue" "+")) -> ("something" "is" "furry" "+"))
If something is white then it is young.
((("something" "is" "white" "+")) -> ("something" "is" "young" "+"))
If Erin is white then Erin is kind.
((("Erin" "is" "white" "+")) -> ("Erin" "is" "kind" "+"))
All furry things are blue.
((("something" "is" "furry" "+")) -> ("something" "is" "blue" "+"))
Charlie is kind.
True
1
proof
[(triple1)]
("Charlie" "is" "kind" "+")
triple1
Erin is not white.
False
1
inv-proof
[(triple4)]
("Erin" "is" "white" "-")
triple4
Erin is young.
True
2
proof
[(((triple4) -> rule7))]
("Erin" "is" "young" "+")
((triple4) -> (rule7 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Gary is not furry.
False
2
inv-proof
[(((triple8) -> rule6))]
("Gary" "is" "furry" "-")
((triple8) -> (rule6 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Charlie is blue.
True
4
proof
[(((((triple1 triple2) -> rule3)) -> rule9))]
("Charlie" "is" "blue" "+")
((((triple1 triple2) -> (rule3 % int2))) -> (rule9 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Gary is not white.
False
4
inv-proof
[(((((triple8) -> rule6) triple10) -> rule2) OR ((((triple8) -> rule6) ((triple8) -> rule4)) -> rule2))]
("Gary" "is" "white" "-")
((((triple8) -> (rule6 % int2)) triple10) -> (rule2 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
((((triple8) -> (rule6 % int3)) ((triple8) -> (rule4 % int2))) -> (rule2 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3
Charlie is rough.
True
5
proof
[(((((((triple1 triple2) -> rule3)) -> rule9)) -> rule4))]
("Charlie" "is" "rough" "+")
((((((triple1 triple2) -> (rule3 % int3))) -> (rule9 % int2))) -> (rule4 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3
Charlie is not rough.
False
5
inv-proof
[(((((((triple1 triple2) -> rule3)) -> rule9)) -> rule4))]
("Charlie" "is" "rough" "-")
((((((triple1 triple2) -> (rule3 % int3))) -> (rule9 % int2))) -> (rule4 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3
Charlie is white.
True
9
proof
[(((((triple1 triple2) -> rule3) ((((((triple1 triple2) -> rule3)) -> rule9)) -> rule4)) -> rule2))]
("Charlie" "is" "white" "+")
((((triple1 triple2) -> (rule3 % int4)) ((((((triple1 triple2) -> (rule3 % int4))) -> (rule9 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Charlie is furry.
("Charlie" "is" "furry" "+")
int4
Charlie is not white.
False
9
inv-proof
[(((((triple1 triple2) -> rule3) ((((((triple1 triple2) -> rule3)) -> rule9)) -> rule4)) -> rule2))]
("Charlie" "is" "white" "-")
((((triple1 triple2) -> (rule3 % int4)) ((((((triple1 triple2) -> (rule3 % int4))) -> (rule9 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Charlie is furry.
("Charlie" "is" "furry" "+")
int4
Charlie is young.
True
10
proof
[(((((((triple1 triple2) -> rule3) ((((((triple1 triple2) -> rule3)) -> rule9)) -> rule4)) -> rule2)) -> rule7))]
("Charlie" "is" "young" "+")
((((((triple1 triple2) -> (rule3 % int5)) ((((((triple1 triple2) -> (rule3 % int5))) -> (rule9 % int4))) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Charlie is blue.
("Charlie" "is" "blue" "+")
int4
Charlie is furry.
("Charlie" "is" "furry" "+")
int5
Charlie is not young.
False
10
inv-proof
[(((((((triple1 triple2) -> rule3) ((((((triple1 triple2) -> rule3)) -> rule9)) -> rule4)) -> rule2)) -> rule7))]
("Charlie" "is" "young" "-")
((((((triple1 triple2) -> (rule3 % int5)) ((((((triple1 triple2) -> (rule3 % int5))) -> (rule9 % int4))) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Charlie is blue.
("Charlie" "is" "blue" "+")
int4
Charlie is furry.
("Charlie" "is" "furry" "+")
int5
Fiona is not white.
Unknown
inv-rconc
[@5: Fiona is white.[CWA. Example of deepest failure = (rule2 <- rule6 <- rule9 <- rule3 <- rule5 <- FAIL)]]
("Fiona" "is" "white" "-")
Erin is rough.
Unknown
rconc
[@3: Erin is rough.[CWA. Example of deepest failure = (rule4 <- rule9 <- rule3 <- FAIL)]]
("Erin" "is" "rough" "+")
Fiona is not kind.
Unknown
inv-rconc
[@4: Fiona is kind.[CWA. Example of deepest failure = (rule5 <- rule6 <- rule9 <- rule3 <- FAIL)]]
("Fiona" "is" "kind" "-")
Erin is furry.
Unknown
rconc
[@3: Erin is furry.[CWA. Example of deepest failure = (rule6 <- rule9 <- rule3 <- FAIL)]]
("Erin" "is" "furry" "+")
Erin is not blue.
Unknown
inv-rconc
[@2: Erin is blue.[CWA. Example of deepest failure = (rule9 <- rule3 <- FAIL)]]
("Erin" "is" "blue" "-")
Fiona is blue.
Unknown
rconc
[@4: Fiona is blue.[CWA. Example of deepest failure = (rule9 <- rule3 <- rule5 <- rule6 <- FAIL)]]
("Fiona" "is" "blue" "+")
Gary is not quiet.
Unknown
inv-random
[@0: Gary is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "quiet" "-")
Erin is quiet.
Unknown
random
[@0: Erin is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "quiet" "+")
@0: Charlie is kind.[(triple1)] Charlie is quiet.[(triple2)] Erin is kind.[(triple3 OR ((triple4) -> rule8))] Erin is white.[(triple4)] Fiona is quiet.[(triple5)] Fiona is rough.[(triple6)] Fiona is young.[(triple7)] Gary is blue.[(triple8)] Gary is kind.[(triple9 OR ((((((triple8) -> rule6) triple10) -> rule2) ((triple8) -> rule6)) -> rule5) OR ((((((triple8) -> rule6) ((triple8) -> rule4)) -> rule2) ((triple8) -> rule6)) -> rule5))] Gary is rough.[(triple10 OR ((triple8) -> rule4))] Gary is young.[(triple11 OR ((((((triple8) -> rule6) triple10) -> rule2)) -> rule7) OR ((((((triple8) -> rule6) ((triple8) -> rule4)) -> rule2)) -> rule7))] @1: Charlie is furry.[(((triple1 triple2) -> rule3))] Erin is young.[(((triple4) -> rule7))] Gary is furry.[(((triple8) -> rule6))] @2: Charlie is blue.[(((((triple1 triple2) -> rule3)) -> rule9))] Gary is white.[(((((triple8) -> rule6) triple10) -> rule2) OR ((((triple8) -> rule6) ((triple8) -> rule4)) -> rule2))] @3: Charlie is rough.[(((((((triple1 triple2) -> rule3)) -> rule9)) -> rule4))] @4: Charlie is white.[(((((triple1 triple2) -> rule3) ((((((triple1 triple2) -> rule3)) -> rule9)) -> rule4)) -> rule2))] @5: Charlie is young.[(((((((triple1 triple2) -> rule3) ((((((triple1 triple2) -> rule3)) -> rule9)) -> rule4)) -> rule2)) -> rule7))]
Charlie is kind.
("Charlie" "is" "kind" "+")
triple1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple2
Erin is kind.
("Erin" "is" "kind" "+")
triple3
((triple4) -> (rule8 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
triple4
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple5
Fiona is rough.
("Fiona" "is" "rough" "+")
triple6
Fiona is young.
("Fiona" "is" "young" "+")
triple7
Gary is blue.
("Gary" "is" "blue" "+")
triple8
Gary is kind.
("Gary" "is" "kind" "+")
triple9
((((((triple8) -> (rule6 % int3)) triple10) -> (rule2 % int2)) ((triple8) -> (rule6 % int3))) -> (rule5 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3
((((((triple8) -> (rule6 % int4)) ((triple8) -> (rule4 % int3))) -> (rule2 % int2)) ((triple8) -> (rule6 % int4))) -> (rule5 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
Gary is furry.
("Gary" "is" "furry" "+")
int4
Gary is rough.
("Gary" "is" "rough" "+")
triple10
((triple8) -> (rule4 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
triple11
((((((triple8) -> (rule6 % int3)) triple10) -> (rule2 % int2))) -> (rule7 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3
((((((triple8) -> (rule6 % int4)) ((triple8) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
Gary is furry.
("Gary" "is" "furry" "+")
int4
Charlie is furry.
("Charlie" "is" "furry" "+")
((triple1 triple2) -> (rule3 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
((triple4) -> (rule7 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
((triple8) -> (rule6 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
((((triple1 triple2) -> (rule3 % int2))) -> (rule9 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
((((triple8) -> (rule6 % int2)) triple10) -> (rule2 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
((((triple8) -> (rule6 % int3)) ((triple8) -> (rule4 % int2))) -> (rule2 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3
Charlie is rough.
("Charlie" "is" "rough" "+")
((((((triple1 triple2) -> (rule3 % int3))) -> (rule9 % int2))) -> (rule4 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3
Charlie is white.
("Charlie" "is" "white" "+")
((((triple1 triple2) -> (rule3 % int4)) ((((((triple1 triple2) -> (rule3 % int4))) -> (rule9 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Charlie is furry.
("Charlie" "is" "furry" "+")
int4
Charlie is young.
("Charlie" "is" "young" "+")
((((((triple1 triple2) -> (rule3 % int5)) ((((((triple1 triple2) -> (rule3 % int5))) -> (rule9 % int4))) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Charlie is blue.
("Charlie" "is" "blue" "+")
int4
Charlie is furry.
("Charlie" "is" "furry" "+")
int5