Anne is rough. Anne is smart. Dave is blue. Dave is furry. Dave is quiet. Dave is not rough. Gary is big. Gary is green. Gary is quiet. Gary is smart. Harry is big. All big things are quiet. All quiet things are furry. If something is rough and not quiet then it is not green. If something is furry then it is green. If Harry is blue then Harry is smart. If something is green and not big then it is blue. All furry things are blue. All smart, green things are rough.
Anne is rough.
("Anne" "is" "rough" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is not rough.
("Dave" "is" "rough" "-")
Gary is big.
("Gary" "is" "big" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Harry is big.
("Harry" "is" "big" "+")
All big things are quiet.
((("something" "is" "big" "+")) -> ("something" "is" "quiet" "+"))
All quiet things are furry.
((("something" "is" "quiet" "+")) -> ("something" "is" "furry" "+"))
If something is rough and not quiet then it is not green.
((("something" "is" "rough" "+") ("something" "is" "quiet" "~")) -> ("something" "is" "green" "-"))
If something is furry then it is green.
((("something" "is" "furry" "+")) -> ("something" "is" "green" "+"))
If Harry is blue then Harry is smart.
((("Harry" "is" "blue" "+")) -> ("Harry" "is" "smart" "+"))
If something is green and not big then it is blue.
((("something" "is" "green" "+") ("something" "is" "big" "~")) -> ("something" "is" "blue" "+"))
All furry things are blue.
((("something" "is" "furry" "+")) -> ("something" "is" "blue" "+"))
All smart, green things are rough.
((("something" "is" "smart" "+") ("something" "is" "green" "+")) -> ("something" "is" "rough" "+"))
Anne is rough.
True
1
proof
[(triple1)]
("Anne" "is" "rough" "+")
triple1
Harry is not big.
False
1
inv-proof
[(triple11)]
("Harry" "is" "big" "-")
triple11
Harry is quiet.
True
2
proof
[(((triple11) -> rule1))]
("Harry" "is" "quiet" "+")
((triple11) -> (rule1 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Gary is not furry.
False
2
inv-proof
[(((triple9) -> rule2) OR ((((triple7) -> rule1)) -> rule2))]
("Gary" "is" "furry" "-")
((triple9) -> (rule2 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
((((triple7) -> (rule1 % int2))) -> (rule2 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is blue.
True
3
proof
[(((((triple9) -> rule2)) -> rule7) OR ((((((triple7) -> rule1)) -> rule2)) -> rule7))]
("Gary" "is" "blue" "+")
((((triple9) -> (rule2 % int2))) -> (rule7 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
((((((triple7) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Gary is not blue.
False
3
inv-proof
[(((((triple9) -> rule2)) -> rule7) OR ((((((triple7) -> rule1)) -> rule2)) -> rule7))]
("Gary" "is" "blue" "-")
((((triple9) -> (rule2 % int2))) -> (rule7 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
((((((triple7) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Harry is green.
True
4
proof
[(((((((triple11) -> rule1)) -> rule2)) -> rule4))]
("Harry" "is" "green" "+")
((((((triple11) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
Harry is not green.
False
4
inv-proof
[(((((((triple11) -> rule1)) -> rule2)) -> rule4))]
("Harry" "is" "green" "-")
((((((triple11) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
Harry is smart.
True
5
proof
[(((((((((triple11) -> rule1)) -> rule2)) -> rule7)) -> rule5))]
("Harry" "is" "smart" "+")
((((((((triple11) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
Harry is quiet.
("Harry" "is" "quiet" "+")
int4
Harry is not smart.
False
5
inv-proof
[(((((((((triple11) -> rule1)) -> rule2)) -> rule7)) -> rule5))]
("Harry" "is" "smart" "-")
((((((((triple11) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
Harry is quiet.
("Harry" "is" "quiet" "+")
int4
Harry is rough.
True
10
proof
[(((((((((((triple11) -> rule1)) -> rule2)) -> rule7)) -> rule5) ((((((triple11) -> rule1)) -> rule2)) -> rule4)) -> rule8))]
("Harry" "is" "rough" "+")
((((((((((triple11) -> (rule1 % int6))) -> (rule2 % int5))) -> (rule7 % int4))) -> (rule5 % int3)) ((((((triple11) -> (rule1 % int6))) -> (rule2 % int5))) -> (rule4 % int2))) -> (rule8 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
Harry is blue.
("Harry" "is" "blue" "+")
int4
Harry is furry.
("Harry" "is" "furry" "+")
int5
Harry is quiet.
("Harry" "is" "quiet" "+")
int6
Harry is not rough.
False
10
inv-proof
[(((((((((((triple11) -> rule1)) -> rule2)) -> rule7)) -> rule5) ((((((triple11) -> rule1)) -> rule2)) -> rule4)) -> rule8))]
("Harry" "is" "rough" "-")
((((((((((triple11) -> (rule1 % int6))) -> (rule2 % int5))) -> (rule7 % int4))) -> (rule5 % int3)) ((((((triple11) -> (rule1 % int6))) -> (rule2 % int5))) -> (rule4 % int2))) -> (rule8 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
Harry is blue.
("Harry" "is" "blue" "+")
int4
Harry is furry.
("Harry" "is" "furry" "+")
int5
Harry is quiet.
("Harry" "is" "quiet" "+")
int6
Anne is not green.
Unknown
inv-rconc
[@3: Anne is green.[CWA. Example of deepest failure = (rule4 <- rule2 <- rule1 <- FAIL)]]
("Anne" "is" "green" "-")
Anne is furry.
Unknown
rconc
[@2: Anne is furry.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("Anne" "is" "furry" "+")
Anne is not blue.
Unknown
inv-rconc
[@3: Anne is blue.[CWA. Example of deepest failure = (rule7 <- rule2 <- rule1 <- FAIL)]]
("Anne" "is" "blue" "-")
Anne is quiet.
Unknown
rconc
[@1: Anne is quiet.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "quiet" "+")
Dave is not big.
Unknown
inv-random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "-")
Dave is smart.
Unknown
random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "+")
@0: Anne is rough.[(triple1)] Anne is smart.[(triple2)] Dave is blue.[(triple3 OR ((triple4) -> rule7) OR ((((triple5) -> rule2)) -> rule7))] Dave is furry.[(triple4 OR ((triple5) -> rule2))] Dave is not rough.[(triple6)] Dave is quiet.[(triple5)] Gary is big.[(triple7)] Gary is green.[(triple8 OR ((((triple9) -> rule2)) -> rule4) OR ((((((triple7) -> rule1)) -> rule2)) -> rule4))] Gary is quiet.[(triple9 OR ((triple7) -> rule1))] Gary is smart.[(triple10)] Harry is big.[(triple11)] @1: Dave is green.[(((triple4) -> rule4) OR ((((triple5) -> rule2)) -> rule4))] Gary is furry.[(((triple9) -> rule2) OR ((((triple7) -> rule1)) -> rule2))] Gary is rough.[(((triple10 triple8) -> rule8) OR ((triple10 ((((triple9) -> rule2)) -> rule4)) -> rule8) OR ((triple10 ((((((triple7) -> rule1)) -> rule2)) -> rule4)) -> rule8))] Harry is quiet.[(((triple11) -> rule1))] @2: Gary is blue.[(((((triple9) -> rule2)) -> rule7) OR ((((((triple7) -> rule1)) -> rule2)) -> rule7))] Harry is furry.[(((((triple11) -> rule1)) -> rule2))] @3: Harry is blue.[(((((((triple11) -> rule1)) -> rule2)) -> rule7))] Harry is green.[(((((((triple11) -> rule1)) -> rule2)) -> rule4))] @4: Harry is smart.[(((((((((triple11) -> rule1)) -> rule2)) -> rule7)) -> rule5))] @5: Harry is rough.[(((((((((((triple11) -> rule1)) -> rule2)) -> rule7)) -> rule5) ((((((triple11) -> rule1)) -> rule2)) -> rule4)) -> rule8))]
Anne is rough.
("Anne" "is" "rough" "+")
triple1
Anne is smart.
("Anne" "is" "smart" "+")
triple2
Dave is blue.
("Dave" "is" "blue" "+")
triple3
((triple4) -> (rule7 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
((((triple5) -> (rule2 % int2))) -> (rule7 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
triple4
((triple5) -> (rule2 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is not rough.
("Dave" "is" "rough" "-")
triple6
Dave is quiet.
("Dave" "is" "quiet" "+")
triple5
Gary is big.
("Gary" "is" "big" "+")
triple7
Gary is green.
("Gary" "is" "green" "+")
triple8
((((triple9) -> (rule2 % int2))) -> (rule4 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
((((((triple7) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Gary is quiet.
("Gary" "is" "quiet" "+")
triple9
((triple7) -> (rule1 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
triple10
Harry is big.
("Harry" "is" "big" "+")
triple11
Dave is green.
("Dave" "is" "green" "+")
((triple4) -> (rule4 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
((((triple5) -> (rule2 % int2))) -> (rule4 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
((triple9) -> (rule2 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
((((triple7) -> (rule1 % int2))) -> (rule2 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
((triple10 triple8) -> (rule8 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
((triple10 ((((triple9) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3
((triple10 ((((((triple7) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3
Gary is quiet.
("Gary" "is" "quiet" "+")
int4
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple11) -> (rule1 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
((((triple9) -> (rule2 % int2))) -> (rule7 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
((((((triple7) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Harry is furry.
("Harry" "is" "furry" "+")
((((triple11) -> (rule1 % int2))) -> (rule2 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
((((((triple11) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
Harry is green.
("Harry" "is" "green" "+")
((((((triple11) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
Harry is smart.
("Harry" "is" "smart" "+")
((((((((triple11) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
Harry is quiet.
("Harry" "is" "quiet" "+")
int4
Harry is rough.
("Harry" "is" "rough" "+")
((((((((((triple11) -> (rule1 % int6))) -> (rule2 % int5))) -> (rule7 % int4))) -> (rule5 % int3)) ((((((triple11) -> (rule1 % int6))) -> (rule2 % int5))) -> (rule4 % int2))) -> (rule8 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
Harry is blue.
("Harry" "is" "blue" "+")
int4
Harry is furry.
("Harry" "is" "furry" "+")
int5
Harry is quiet.
("Harry" "is" "quiet" "+")
int6