Charlie is cold. Charlie is kind. Charlie is rough. Charlie is white. Gary is cold. Gary is furry. Harry is furry. Harry is kind. Harry is red. Harry is white. If someone is furry then they are kind. If someone is young then they are white. If Charlie is young and Charlie is white then Charlie is red. White, furry people are red. All cold, young people are kind. If Charlie is furry and Charlie is kind then Charlie is cold. If someone is kind then they are rough. Cold, kind people are young.
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is white.
("Harry" "is" "white" "+")
If someone is furry then they are kind.
((("someone" "is" "furry" "+")) -> ("someone" "is" "kind" "+"))
If someone is young then they are white.
((("someone" "is" "young" "+")) -> ("someone" "is" "white" "+"))
If Charlie is young and Charlie is white then Charlie is red.
((("Charlie" "is" "young" "+") ("Charlie" "is" "white" "+")) -> ("Charlie" "is" "red" "+"))
White, furry people are red.
((("someone" "is" "white" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "red" "+"))
All cold, young people are kind.
((("someone" "is" "cold" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "kind" "+"))
If Charlie is furry and Charlie is kind then Charlie is cold.
((("Charlie" "is" "furry" "+") ("Charlie" "is" "kind" "+")) -> ("Charlie" "is" "cold" "+"))
If someone is kind then they are rough.
((("someone" "is" "kind" "+")) -> ("someone" "is" "rough" "+"))
Cold, kind people are young.
((("someone" "is" "cold" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "young" "+"))
Charlie is rough.
True
1
proof
[(triple3 OR ((triple2) -> rule7))]
("Charlie" "is" "rough" "+")
triple3
((triple2) -> (rule7 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is not kind.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "kind" "-")
triple2
Harry is rough.
True
2
proof
[(((triple8) -> rule7) OR ((((triple7) -> rule1)) -> rule7))]
("Harry" "is" "rough" "+")
((triple8) -> (rule7 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
((((triple7) -> (rule1 % int2))) -> (rule7 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Charlie is not young.
False
3
inv-proof
[(((triple1 triple2) -> rule8))]
("Charlie" "is" "young" "-")
((triple1 triple2) -> (rule8 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Gary is rough.
True
3
proof
[(((((triple6) -> rule1)) -> rule7))]
("Gary" "is" "rough" "+")
((((triple6) -> (rule1 % int2))) -> (rule7 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is not young.
False
4
inv-proof
[(((triple5 ((triple6) -> rule1)) -> rule8))]
("Gary" "is" "young" "-")
((triple5 ((triple6) -> (rule1 % int2))) -> (rule8 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is white.
True
5
proof
[(((((triple5 ((triple6) -> rule1)) -> rule8)) -> rule2))]
("Gary" "is" "white" "+")
((((triple5 ((triple6) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3
Gary is not white.
False
5
inv-proof
[(((((triple5 ((triple6) -> rule1)) -> rule8)) -> rule2))]
("Gary" "is" "white" "-")
((((triple5 ((triple6) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3
Harry is not young.
Unknown
inv-rconc
[@1: Harry is young.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Harry" "is" "young" "-")
Harry is cold.
Unknown
random
[@0: Harry is cold.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "cold" "+")
@0: Charlie is cold.[(triple1)] Charlie is kind.[(triple2)] Charlie is rough.[(triple3 OR ((triple2) -> rule7))] Charlie is white.[(triple4 OR ((((triple1 triple2) -> rule8)) -> rule2))] Gary is cold.[(triple5)] Gary is furry.[(triple6)] Harry is furry.[(triple7)] Harry is kind.[(triple8 OR ((triple7) -> rule1))] Harry is red.[(triple9 OR ((triple10 triple7) -> rule4))] Harry is white.[(triple10)] @1: Charlie is young.[(((triple1 triple2) -> rule8))] Gary is kind.[(((triple6) -> rule1))] Harry is rough.[(((triple8) -> rule7) OR ((((triple7) -> rule1)) -> rule7))] @2: Charlie is red.[(((((triple1 triple2) -> rule8) triple4) -> rule3) OR ((((triple1 triple2) -> rule8) ((((triple1 triple2) -> rule8)) -> rule2)) -> rule3))] Gary is rough.[(((((triple6) -> rule1)) -> rule7))] Gary is young.[(((triple5 ((triple6) -> rule1)) -> rule8))] @3: Gary is white.[(((((triple5 ((triple6) -> rule1)) -> rule8)) -> rule2))] @4: Gary is red.[(((((((triple5 ((triple6) -> rule1)) -> rule8)) -> rule2) triple6) -> rule4))]
Charlie is cold.
("Charlie" "is" "cold" "+")
triple1
Charlie is kind.
("Charlie" "is" "kind" "+")
triple2
Charlie is rough.
("Charlie" "is" "rough" "+")
triple3
((triple2) -> (rule7 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
triple4
((((triple1 triple2) -> (rule8 % int2))) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
triple5
Gary is furry.
("Gary" "is" "furry" "+")
triple6
Harry is furry.
("Harry" "is" "furry" "+")
triple7
Harry is kind.
("Harry" "is" "kind" "+")
triple8
((triple7) -> (rule1 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
triple9
((triple10 triple7) -> (rule4 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
triple10
Charlie is young.
("Charlie" "is" "young" "+")
((triple1 triple2) -> (rule8 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
((triple6) -> (rule1 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
((triple8) -> (rule7 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
((((triple7) -> (rule1 % int2))) -> (rule7 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
((((triple1 triple2) -> (rule8 % int2)) triple4) -> (rule3 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
((((triple1 triple2) -> (rule8 % int3)) ((((triple1 triple2) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3
Gary is rough.
("Gary" "is" "rough" "+")
((((triple6) -> (rule1 % int2))) -> (rule7 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
((triple5 ((triple6) -> (rule1 % int2))) -> (rule8 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
((((triple5 ((triple6) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3
Gary is red.
("Gary" "is" "red" "+")
((((((triple5 ((triple6) -> (rule1 % int4))) -> (rule8 % int3))) -> (rule2 % int2)) triple6) -> (rule4 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
int3
Gary is kind.
("Gary" "is" "kind" "+")
int4