Charlie is green. Charlie is nice. Charlie is rough. Charlie is white. Harry is rough. Harry is round. Harry is white. Round, furry things are rough. Round, white things are nice. Rough, round things are nice. If something is nice then it is furry. All green things are not round. If something is rough and not green then it is round. If Charlie is furry and Charlie is not green then Charlie is big. If Harry is furry then Harry is big.
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is white.
("Harry" "is" "white" "+")
Round, furry things are rough.
((("something" "is" "round" "+") ("something" "is" "furry" "+")) -> ("something" "is" "rough" "+"))
Round, white things are nice.
((("something" "is" "round" "+") ("something" "is" "white" "+")) -> ("something" "is" "nice" "+"))
Rough, round things are nice.
((("something" "is" "rough" "+") ("something" "is" "round" "+")) -> ("something" "is" "nice" "+"))
If something is nice then it is furry.
((("something" "is" "nice" "+")) -> ("something" "is" "furry" "+"))
All green things are not round.
((("something" "is" "green" "+")) -> ("something" "is" "round" "-"))
If something is rough and not green then it is round.
((("something" "is" "rough" "+") ("something" "is" "green" "~")) -> ("something" "is" "round" "+"))
If Charlie is furry and Charlie is not green then Charlie is big.
((("Charlie" "is" "furry" "+") ("Charlie" "is" "green" "~")) -> ("Charlie" "is" "big" "+"))
If Harry is furry then Harry is big.
((("Harry" "is" "furry" "+")) -> ("Harry" "is" "big" "+"))
Harry is rough.
True
1
proof
[(triple5 OR ((triple6 ((((triple6 triple7) -> rule2)) -> rule4)) -> rule1))]
("Harry" "is" "rough" "+")
triple5
((triple6 ((((triple6 triple7) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Harry is not round.
False
1
inv-proof
[(triple6)]
("Harry" "is" "round" "-")
triple6
Charlie is furry.
True
2
proof
[(((triple2) -> rule4))]
("Charlie" "is" "furry" "+")
((triple2) -> (rule4 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Harry is not nice.
False
3
inv-proof
[(((triple5 triple6) -> rule3) OR ((triple6 triple7) -> rule2))]
("Harry" "is" "nice" "-")
((triple5 triple6) -> (rule3 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
((triple6 triple7) -> (rule2 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is furry.
True
4
proof
[(((((triple5 triple6) -> rule3)) -> rule4) OR ((((triple6 triple7) -> rule2)) -> rule4))]
("Harry" "is" "furry" "+")
((((triple5 triple6) -> (rule3 % int2))) -> (rule4 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
((((triple6 triple7) -> (rule2 % int2))) -> (rule4 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is not furry.
False
4
inv-proof
[(((((triple5 triple6) -> rule3)) -> rule4) OR ((((triple6 triple7) -> rule2)) -> rule4))]
("Harry" "is" "furry" "-")
((((triple5 triple6) -> (rule3 % int2))) -> (rule4 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
((((triple6 triple7) -> (rule2 % int2))) -> (rule4 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is big.
True
5
proof
[(((((((triple5 triple6) -> rule3)) -> rule4)) -> rule8) OR ((((((triple6 triple7) -> rule2)) -> rule4)) -> rule8))]
("Harry" "is" "big" "+")
((((((triple5 triple6) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
((((((triple6 triple7) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Harry is not big.
False
5
inv-proof
[(((((((triple5 triple6) -> rule3)) -> rule4)) -> rule8) OR ((((((triple6 triple7) -> rule2)) -> rule4)) -> rule8))]
("Harry" "is" "big" "-")
((((((triple5 triple6) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
((((((triple6 triple7) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Charlie is not big.
Unknown
inv-rconc
[@1: Charlie is big.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Charlie" "is" "big" "-")
Harry is green.
Unknown
random
[@0: Harry is green.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "green" "+")
@0: Charlie is green.[(triple1)] Charlie is nice.[(triple2)] Charlie is rough.[(triple3)] Charlie is white.[(triple4)] Harry is rough.[(triple5 OR ((triple6 ((((triple6 triple7) -> rule2)) -> rule4)) -> rule1))] Harry is round.[(triple6)] Harry is white.[(triple7)] @1: Charlie is furry.[(((triple2) -> rule4))] Charlie is not round.[(((triple1) -> rule5))] Harry is nice.[(((triple5 triple6) -> rule3) OR ((triple6 triple7) -> rule2))] @2: Harry is furry.[(((((triple5 triple6) -> rule3)) -> rule4) OR ((((triple6 triple7) -> rule2)) -> rule4))] @3: Harry is big.[(((((((triple5 triple6) -> rule3)) -> rule4)) -> rule8) OR ((((((triple6 triple7) -> rule2)) -> rule4)) -> rule8))]
Charlie is green.
("Charlie" "is" "green" "+")
triple1
Charlie is nice.
("Charlie" "is" "nice" "+")
triple2
Charlie is rough.
("Charlie" "is" "rough" "+")
triple3
Charlie is white.
("Charlie" "is" "white" "+")
triple4
Harry is rough.
("Harry" "is" "rough" "+")
triple5
((triple6 ((((triple6 triple7) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Harry is round.
("Harry" "is" "round" "+")
triple6
Harry is white.
("Harry" "is" "white" "+")
triple7
Charlie is furry.
("Charlie" "is" "furry" "+")
((triple2) -> (rule4 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is not round.
("Charlie" "is" "round" "-")
((triple1) -> (rule5 % int1))
Charlie is not round.
("Charlie" "is" "round" "-")
int1
Harry is nice.
("Harry" "is" "nice" "+")
((triple5 triple6) -> (rule3 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
((triple6 triple7) -> (rule2 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
((((triple5 triple6) -> (rule3 % int2))) -> (rule4 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
((((triple6 triple7) -> (rule2 % int2))) -> (rule4 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
((((((triple5 triple6) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
((((((triple6 triple7) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3