Charlie is furry. Charlie is green. Charlie is not young. Dave is young. Gary is not blue. Gary is not furry. Gary is smart. Harry is blue. Harry is green. Harry is quiet. If someone is furry and young then they are green. Young, green people are rough. If someone is blue then they are furry. Young people are blue. If Charlie is furry and Charlie is young then Charlie is smart. If Dave is furry then Dave is smart. If someone is quiet then they are smart. Smart, rough people are quiet.
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is not young.
("Charlie" "is" "young" "-")
Dave is young.
("Dave" "is" "young" "+")
Gary is not blue.
("Gary" "is" "blue" "-")
Gary is not furry.
("Gary" "is" "furry" "-")
Gary is smart.
("Gary" "is" "smart" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
If someone is furry and young then they are green.
((("someone" "is" "furry" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "green" "+"))
Young, green people are rough.
((("someone" "is" "young" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "rough" "+"))
If someone is blue then they are furry.
((("someone" "is" "blue" "+")) -> ("someone" "is" "furry" "+"))
Young people are blue.
((("someone" "is" "young" "+")) -> ("someone" "is" "blue" "+"))
If Charlie is furry and Charlie is young then Charlie is smart.
((("Charlie" "is" "furry" "+") ("Charlie" "is" "young" "+")) -> ("Charlie" "is" "smart" "+"))
If Dave is furry then Dave is smart.
((("Dave" "is" "furry" "+")) -> ("Dave" "is" "smart" "+"))
If someone is quiet then they are smart.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "smart" "+"))
Smart, rough people are quiet.
((("someone" "is" "smart" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "quiet" "+"))
Harry is green.
True
1
proof
[(triple9)]
("Harry" "is" "green" "+")
triple9
Gary is furry.
False
1
inv-proof
[(triple6)]
("Gary" "is" "furry" "+")
triple6
Dave is blue.
True
2
proof
[(((triple4) -> rule4))]
("Dave" "is" "blue" "+")
((triple4) -> (rule4 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Harry is not smart.
False
2
inv-proof
[(((triple10) -> rule7))]
("Harry" "is" "smart" "-")
((triple10) -> (rule7 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Dave is furry.
True
3
proof
[(((((triple4) -> rule4)) -> rule3))]
("Dave" "is" "furry" "+")
((((triple4) -> (rule4 % int2))) -> (rule3 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is not furry.
False
3
inv-proof
[(((((triple4) -> rule4)) -> rule3))]
("Dave" "is" "furry" "-")
((((triple4) -> (rule4 % int2))) -> (rule3 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is green.
True
5
proof
[(((((((triple4) -> rule4)) -> rule3) triple4) -> rule1))]
("Dave" "is" "green" "+")
((((((triple4) -> (rule4 % int3))) -> (rule3 % int2)) triple4) -> (rule1 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Dave is not green.
False
5
inv-proof
[(((((((triple4) -> rule4)) -> rule3) triple4) -> rule1))]
("Dave" "is" "green" "-")
((((((triple4) -> (rule4 % int3))) -> (rule3 % int2)) triple4) -> (rule1 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Dave is rough.
True
7
proof
[(((triple4 ((((((triple4) -> rule4)) -> rule3) triple4) -> rule1)) -> rule2))]
("Dave" "is" "rough" "+")
((triple4 ((((((triple4) -> (rule4 % int4))) -> (rule3 % int3)) triple4) -> (rule1 % int2))) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Dave is blue.
("Dave" "is" "blue" "+")
int4
Dave is not rough.
False
7
inv-proof
[(((triple4 ((((((triple4) -> rule4)) -> rule3) triple4) -> rule1)) -> rule2))]
("Dave" "is" "rough" "-")
((triple4 ((((((triple4) -> (rule4 % int4))) -> (rule3 % int3)) triple4) -> (rule1 % int2))) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Dave is blue.
("Dave" "is" "blue" "+")
int4
Dave is quiet.
True
12
proof
[(((((((((triple4) -> rule4)) -> rule3)) -> rule6) ((triple4 ((((((triple4) -> rule4)) -> rule3) triple4) -> rule1)) -> rule2)) -> rule8))]
("Dave" "is" "quiet" "+")
((((((((triple4) -> (rule4 % int6))) -> (rule3 % int5))) -> (rule6 % int4)) ((triple4 ((((((triple4) -> (rule4 % int6))) -> (rule3 % int5)) triple4) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Dave is smart.
("Dave" "is" "smart" "+")
int4
Dave is furry.
("Dave" "is" "furry" "+")
int5
Dave is blue.
("Dave" "is" "blue" "+")
int6
Dave is not quiet.
False
12
inv-proof
[(((((((((triple4) -> rule4)) -> rule3)) -> rule6) ((triple4 ((((((triple4) -> rule4)) -> rule3) triple4) -> rule1)) -> rule2)) -> rule8))]
("Dave" "is" "quiet" "-")
((((((((triple4) -> (rule4 % int6))) -> (rule3 % int5))) -> (rule6 % int4)) ((triple4 ((((((triple4) -> (rule4 % int6))) -> (rule3 % int5)) triple4) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Dave is smart.
("Dave" "is" "smart" "+")
int4
Dave is furry.
("Dave" "is" "furry" "+")
int5
Dave is blue.
("Dave" "is" "blue" "+")
int6
Harry is not rough.
Unknown
inv-rconc
[@1: Harry is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Harry" "is" "rough" "-")
Charlie is smart.
Unknown
rconc
[@3: Charlie is smart.[CWA. Example of deepest failure = (rule7 <- rule8 <- rule5 <- FAIL)]]
("Charlie" "is" "smart" "+")
Charlie is not quiet.
Unknown
inv-rconc
[@2: Charlie is quiet.[CWA. Example of deepest failure = (rule8 <- rule5 <- FAIL)]]
("Charlie" "is" "quiet" "-")
Charlie is rough.
Unknown
rconc
[@1: Charlie is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "rough" "+")
Gary is not green.
Unknown
inv-rconc
[@1: Gary is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "green" "-")
Gary is rough.
Unknown
rconc
[@1: Gary is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "rough" "+")
Harry is not young.
Unknown
inv-random
[@0: Harry is young.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "young" "-")
Gary is young.
Unknown
random
[@0: Gary is young.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "young" "+")
@0: Charlie is furry.[(triple1)] Charlie is green.[(triple2)] Charlie is not young.[(triple3)] Dave is young.[(triple4)] Gary is not blue.[(triple5)] Gary is not furry.[(triple6)] Gary is smart.[(triple7)] Harry is blue.[(triple8)] Harry is green.[(triple9)] Harry is quiet.[(triple10)] @1: Dave is blue.[(((triple4) -> rule4))] Harry is furry.[(((triple8) -> rule3))] Harry is smart.[(((triple10) -> rule7))] @2: Dave is furry.[(((((triple4) -> rule4)) -> rule3))] @3: Dave is green.[(((((((triple4) -> rule4)) -> rule3) triple4) -> rule1))] Dave is smart.[(((((((triple4) -> rule4)) -> rule3)) -> rule6))] @4: Dave is rough.[(((triple4 ((((((triple4) -> rule4)) -> rule3) triple4) -> rule1)) -> rule2))] @5: Dave is quiet.[(((((((((triple4) -> rule4)) -> rule3)) -> rule6) ((triple4 ((((((triple4) -> rule4)) -> rule3) triple4) -> rule1)) -> rule2)) -> rule8))]
Charlie is furry.
("Charlie" "is" "furry" "+")
triple1
Charlie is green.
("Charlie" "is" "green" "+")
triple2
Charlie is not young.
("Charlie" "is" "young" "-")
triple3
Dave is young.
("Dave" "is" "young" "+")
triple4
Gary is not blue.
("Gary" "is" "blue" "-")
triple5
Gary is not furry.
("Gary" "is" "furry" "-")
triple6
Gary is smart.
("Gary" "is" "smart" "+")
triple7
Harry is blue.
("Harry" "is" "blue" "+")
triple8
Harry is green.
("Harry" "is" "green" "+")
triple9
Harry is quiet.
("Harry" "is" "quiet" "+")
triple10
Dave is blue.
("Dave" "is" "blue" "+")
((triple4) -> (rule4 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
((triple8) -> (rule3 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
((triple10) -> (rule7 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
((((triple4) -> (rule4 % int2))) -> (rule3 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
((((((triple4) -> (rule4 % int3))) -> (rule3 % int2)) triple4) -> (rule1 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Dave is smart.
("Dave" "is" "smart" "+")
((((((triple4) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Dave is rough.
("Dave" "is" "rough" "+")
((triple4 ((((((triple4) -> (rule4 % int4))) -> (rule3 % int3)) triple4) -> (rule1 % int2))) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Dave is blue.
("Dave" "is" "blue" "+")
int4
Dave is quiet.
("Dave" "is" "quiet" "+")
((((((((triple4) -> (rule4 % int6))) -> (rule3 % int5))) -> (rule6 % int4)) ((triple4 ((((((triple4) -> (rule4 % int6))) -> (rule3 % int5)) triple4) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Dave is smart.
("Dave" "is" "smart" "+")
int4
Dave is furry.
("Dave" "is" "furry" "+")
int5
Dave is blue.
("Dave" "is" "blue" "+")
int6