Charlie is not blue. Charlie is white. Erin is furry. Gary is not quiet. Gary is rough. Gary is not young. Harry is quiet. All white things are green. Quiet things are green. Quiet, rough things are young. Quiet, white things are not blue. If something is blue and white then it is rough. If something is furry then it is rough. If Gary is young then Gary is rough. If Harry is young and Harry is quiet then Harry is not white. Green things are furry.
Charlie is not blue.
("Charlie" "is" "blue" "-")
Charlie is white.
("Charlie" "is" "white" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Gary is not quiet.
("Gary" "is" "quiet" "-")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is not young.
("Gary" "is" "young" "-")
Harry is quiet.
("Harry" "is" "quiet" "+")
All white things are green.
((("something" "is" "white" "+")) -> ("something" "is" "green" "+"))
Quiet things are green.
((("something" "is" "quiet" "+")) -> ("something" "is" "green" "+"))
Quiet, rough things are young.
((("something" "is" "quiet" "+") ("something" "is" "rough" "+")) -> ("something" "is" "young" "+"))
Quiet, white things are not blue.
((("something" "is" "quiet" "+") ("something" "is" "white" "+")) -> ("something" "is" "blue" "-"))
If something is blue and white then it is rough.
((("something" "is" "blue" "+") ("something" "is" "white" "+")) -> ("something" "is" "rough" "+"))
If something is furry then it is rough.
((("something" "is" "furry" "+")) -> ("something" "is" "rough" "+"))
If Gary is young then Gary is rough.
((("Gary" "is" "young" "+")) -> ("Gary" "is" "rough" "+"))
If Harry is young and Harry is quiet then Harry is not white.
((("Harry" "is" "young" "+") ("Harry" "is" "quiet" "+")) -> ("Harry" "is" "white" "-"))
Green things are furry.
((("something" "is" "green" "+")) -> ("something" "is" "furry" "+"))
Erin is furry.
True
1
proof
[(triple3)]
("Erin" "is" "furry" "+")
triple3
Gary is young.
False
1
inv-proof
[(triple6)]
("Gary" "is" "young" "+")
triple6
Harry is green.
True
2
proof
[(((triple7) -> rule2))]
("Harry" "is" "green" "+")
((triple7) -> (rule2 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Charlie is not green.
False
2
inv-proof
[(((triple2) -> rule1))]
("Charlie" "is" "green" "-")
((triple2) -> (rule1 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Harry is furry.
True
3
proof
[(((((triple7) -> rule2)) -> rule9))]
("Harry" "is" "furry" "+")
((((triple7) -> (rule2 % int2))) -> (rule9 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is not furry.
False
3
inv-proof
[(((((triple7) -> rule2)) -> rule9))]
("Harry" "is" "furry" "-")
((((triple7) -> (rule2 % int2))) -> (rule9 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is rough.
True
4
proof
[(((((((triple7) -> rule2)) -> rule9)) -> rule6))]
("Harry" "is" "rough" "+")
((((((triple7) -> (rule2 % int3))) -> (rule9 % int2))) -> (rule6 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
Harry is not rough.
False
4
inv-proof
[(((((((triple7) -> rule2)) -> rule9)) -> rule6))]
("Harry" "is" "rough" "-")
((((((triple7) -> (rule2 % int3))) -> (rule9 % int2))) -> (rule6 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
Harry is young.
True
6
proof
[(((triple7 ((((((triple7) -> rule2)) -> rule9)) -> rule6)) -> rule3))]
("Harry" "is" "young" "+")
((triple7 ((((((triple7) -> (rule2 % int4))) -> (rule9 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
Harry is green.
("Harry" "is" "green" "+")
int4
Harry is not young.
False
6
inv-proof
[(((triple7 ((((((triple7) -> rule2)) -> rule9)) -> rule6)) -> rule3))]
("Harry" "is" "young" "-")
((triple7 ((((((triple7) -> (rule2 % int4))) -> (rule9 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
Harry is green.
("Harry" "is" "green" "+")
int4
Harry is not white.
True
8
proof
[(((((triple7 ((((((triple7) -> rule2)) -> rule9)) -> rule6)) -> rule3) triple7) -> rule8))]
("Harry" "is" "white" "-")
((((triple7 ((((((triple7) -> (rule2 % int5))) -> (rule9 % int4))) -> (rule6 % int3))) -> (rule3 % int2)) triple7) -> (rule8 % int1))
Harry is not white.
("Harry" "is" "white" "-")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Harry is furry.
("Harry" "is" "furry" "+")
int4
Harry is green.
("Harry" "is" "green" "+")
int5
Harry is white.
False
8
inv-proof
[(((((triple7 ((((((triple7) -> rule2)) -> rule9)) -> rule6)) -> rule3) triple7) -> rule8))]
("Harry" "is" "white" "+")
((((triple7 ((((((triple7) -> (rule2 % int5))) -> (rule9 % int4))) -> (rule6 % int3))) -> (rule3 % int2)) triple7) -> (rule8 % int1))
Harry is not white.
("Harry" "is" "white" "-")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Harry is furry.
("Harry" "is" "furry" "+")
int4
Harry is green.
("Harry" "is" "green" "+")
int5
Gary is not furry.
Unknown
inv-rconc
[@2: Gary is furry.[CWA. Example of deepest failure = (rule9 <- rule1 <- FAIL)]]
("Gary" "is" "furry" "-")
Erin is young.
Unknown
rconc
[@1: Erin is young.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Erin" "is" "young" "+")
Gary is not green.
Unknown
inv-rconc
[@1: Gary is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "green" "-")
Erin is green.
Unknown
rconc
[@1: Erin is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "green" "+")
Charlie is not young.
Unknown
inv-rconc
[@1: Charlie is young.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "young" "-")
Gary is white.
Unknown
random
[@0: Gary is white.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "white" "+")
Charlie is not quiet.
Unknown
inv-random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "-")
Gary is blue.
Unknown
random
[@0: Gary is blue.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "blue" "+")
Erin is not blue.
Unknown
inv-random
[@0: Erin is blue.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "blue" "-")
Erin is quiet.
Unknown
random
[@0: Erin is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "quiet" "+")
Erin is not white.
Unknown
inv-random
[@0: Erin is white.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "white" "-")
Harry is blue.
Unknown
random
[@0: Harry is blue.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "blue" "+")
@0: Charlie is not blue.[(triple1)] Charlie is white.[(triple2)] Erin is furry.[(triple3)] Gary is not quiet.[(triple4)] Gary is not young.[(triple6)] Gary is rough.[(triple5)] Harry is quiet.[(triple7)] @1: Charlie is green.[(((triple2) -> rule1))] Erin is rough.[(((triple3) -> rule6))] Harry is green.[(((triple7) -> rule2))] @2: Charlie is furry.[(((((triple2) -> rule1)) -> rule9))] Harry is furry.[(((((triple7) -> rule2)) -> rule9))] @3: Charlie is rough.[(((((((triple2) -> rule1)) -> rule9)) -> rule6))] Harry is rough.[(((((((triple7) -> rule2)) -> rule9)) -> rule6))] @4: Harry is young.[(((triple7 ((((((triple7) -> rule2)) -> rule9)) -> rule6)) -> rule3))] @5: Harry is not white.[(((((triple7 ((((((triple7) -> rule2)) -> rule9)) -> rule6)) -> rule3) triple7) -> rule8))]
Charlie is not blue.
("Charlie" "is" "blue" "-")
triple1
Charlie is white.
("Charlie" "is" "white" "+")
triple2
Erin is furry.
("Erin" "is" "furry" "+")
triple3
Gary is not quiet.
("Gary" "is" "quiet" "-")
triple4
Gary is not young.
("Gary" "is" "young" "-")
triple6
Gary is rough.
("Gary" "is" "rough" "+")
triple5
Harry is quiet.
("Harry" "is" "quiet" "+")
triple7
Charlie is green.
("Charlie" "is" "green" "+")
((triple2) -> (rule1 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
((triple3) -> (rule6 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
((triple7) -> (rule2 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
((((triple2) -> (rule1 % int2))) -> (rule9 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
((((triple7) -> (rule2 % int2))) -> (rule9 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
((((((triple2) -> (rule1 % int3))) -> (rule9 % int2))) -> (rule6 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
Harry is rough.
("Harry" "is" "rough" "+")
((((((triple7) -> (rule2 % int3))) -> (rule9 % int2))) -> (rule6 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
Harry is young.
("Harry" "is" "young" "+")
((triple7 ((((((triple7) -> (rule2 % int4))) -> (rule9 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
Harry is green.
("Harry" "is" "green" "+")
int4
Harry is not white.
("Harry" "is" "white" "-")
((((triple7 ((((((triple7) -> (rule2 % int5))) -> (rule9 % int4))) -> (rule6 % int3))) -> (rule3 % int2)) triple7) -> (rule8 % int1))
Harry is not white.
("Harry" "is" "white" "-")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Harry is furry.
("Harry" "is" "furry" "+")
int4
Harry is green.
("Harry" "is" "green" "+")
int5