Bob is blue. Bob is cold. Bob is not green. Bob is kind. Bob is not nice. Bob is smart. Gary is blue. Gary is furry. Gary is green. Harry is blue. Harry is not cold. Harry is furry. Harry is green. Harry is kind. Harry is nice. Harry is smart. Green people are furry. Furry people are nice. If someone is green then they are nice. If Gary is not blue then Gary is furry. If someone is kind and not furry then they are not cold. Kind people are smart. Nice, furry people are kind. If someone is green and not furry then they are kind.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is not green.
("Bob" "is" "green" "-")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is not nice.
("Bob" "is" "nice" "-")
Bob is smart.
("Bob" "is" "smart" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is green.
("Gary" "is" "green" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is not cold.
("Harry" "is" "cold" "-")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Green people are furry.
((("someone" "is" "green" "+")) -> ("someone" "is" "furry" "+"))
Furry people are nice.
((("someone" "is" "furry" "+")) -> ("someone" "is" "nice" "+"))
If someone is green then they are nice.
((("someone" "is" "green" "+")) -> ("someone" "is" "nice" "+"))
If Gary is not blue then Gary is furry.
((("Gary" "is" "blue" "~")) -> ("Gary" "is" "furry" "+"))
If someone is kind and not furry then they are not cold.
((("someone" "is" "kind" "+") ("someone" "is" "furry" "~")) -> ("someone" "is" "cold" "-"))
Kind people are smart.
((("someone" "is" "kind" "+")) -> ("someone" "is" "smart" "+"))
Nice, furry people are kind.
((("someone" "is" "nice" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "kind" "+"))
If someone is green and not furry then they are kind.
((("someone" "is" "green" "+") ("someone" "is" "furry" "~")) -> ("someone" "is" "kind" "+"))
Bob is kind.
True
1
proof
[(triple4)]
("Bob" "is" "kind" "+")
triple4
Gary is not furry.
False
1
inv-proof
[(triple8 OR ((triple9) -> rule1))]
("Gary" "is" "furry" "-")
triple8
((triple9) -> (rule1 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is nice.
True
2
proof
[(((triple8) -> rule2) OR ((triple9) -> rule3) OR ((((triple9) -> rule1)) -> rule2))]
("Gary" "is" "nice" "+")
((triple8) -> (rule2 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
((triple9) -> (rule3 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
((((triple9) -> (rule1 % int2))) -> (rule2 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is not nice.
False
2
inv-proof
[(((triple8) -> rule2) OR ((triple9) -> rule3) OR ((((triple9) -> rule1)) -> rule2))]
("Gary" "is" "nice" "-")
((triple8) -> (rule2 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
((triple9) -> (rule3 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
((((triple9) -> (rule1 % int2))) -> (rule2 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Bob is not furry.
Unknown
inv-rconc
[@1: Bob is furry.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "furry" "-")
Gary is cold.
Unknown
random
[@0: Gary is cold.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "cold" "+")
@0: Bob is blue.[(triple1)] Bob is cold.[(triple2)] Bob is kind.[(triple4)] Bob is not green.[(triple3)] Bob is not nice.[(triple5)] Bob is smart.[(triple6 OR ((triple4) -> rule6))] Gary is blue.[(triple7)] Gary is furry.[(triple8 OR ((triple9) -> rule1))] Gary is green.[(triple9)] Harry is blue.[(triple10)] Harry is furry.[(triple12 OR ((triple13) -> rule1))] Harry is green.[(triple13)] Harry is kind.[(triple14 OR ((triple15 triple12) -> rule7) OR ((triple15 ((triple13) -> rule1)) -> rule7) OR ((((triple12) -> rule2) triple12) -> rule7) OR ((((triple13) -> rule3) triple12) -> rule7) OR ((((triple12) -> rule2) ((triple13) -> rule1)) -> rule7) OR ((((triple13) -> rule3) ((triple13) -> rule1)) -> rule7) OR ((((((triple13) -> rule1)) -> rule2) triple12) -> rule7) OR ((((((triple13) -> rule1)) -> rule2) ((triple13) -> rule1)) -> rule7))] Harry is nice.[(triple15 OR ((triple12) -> rule2) OR ((triple13) -> rule3) OR ((((triple13) -> rule1)) -> rule2))] Harry is not cold.[(triple11)] Harry is smart.[(triple16 OR ((triple14) -> rule6) OR ((((triple15 triple12) -> rule7)) -> rule6) OR ((((triple15 ((triple13) -> rule1)) -> rule7)) -> rule6) OR ((((((triple12) -> rule2) triple12) -> rule7)) -> rule6) OR ((((((triple13) -> rule3) triple12) -> rule7)) -> rule6) OR ((((((triple12) -> rule2) ((triple13) -> rule1)) -> rule7)) -> rule6) OR ((((((triple13) -> rule3) ((triple13) -> rule1)) -> rule7)) -> rule6) OR ((((((((triple13) -> rule1)) -> rule2) triple12) -> rule7)) -> rule6) OR ((((((((triple13) -> rule1)) -> rule2) ((triple13) -> rule1)) -> rule7)) -> rule6))] @1: Gary is nice.[(((triple8) -> rule2) OR ((triple9) -> rule3) OR ((((triple9) -> rule1)) -> rule2))] @2: Gary is kind.[(((((triple8) -> rule2) triple8) -> rule7) OR ((((triple9) -> rule3) triple8) -> rule7) OR ((((triple8) -> rule2) ((triple9) -> rule1)) -> rule7) OR ((((triple9) -> rule3) ((triple9) -> rule1)) -> rule7) OR ((((((triple9) -> rule1)) -> rule2) triple8) -> rule7) OR ((((((triple9) -> rule1)) -> rule2) ((triple9) -> rule1)) -> rule7))] @3: Gary is smart.[(((((((triple8) -> rule2) triple8) -> rule7)) -> rule6) OR ((((((triple9) -> rule3) triple8) -> rule7)) -> rule6) OR ((((((triple8) -> rule2) ((triple9) -> rule1)) -> rule7)) -> rule6) OR ((((((triple9) -> rule3) ((triple9) -> rule1)) -> rule7)) -> rule6) OR ((((((((triple9) -> rule1)) -> rule2) triple8) -> rule7)) -> rule6) OR ((((((((triple9) -> rule1)) -> rule2) ((triple9) -> rule1)) -> rule7)) -> rule6))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is cold.
("Bob" "is" "cold" "+")
triple2
Bob is kind.
("Bob" "is" "kind" "+")
triple4
Bob is not green.
("Bob" "is" "green" "-")
triple3
Bob is not nice.
("Bob" "is" "nice" "-")
triple5
Bob is smart.
("Bob" "is" "smart" "+")
triple6
((triple4) -> (rule6 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
triple7
Gary is furry.
("Gary" "is" "furry" "+")
triple8
((triple9) -> (rule1 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
triple9
Harry is blue.
("Harry" "is" "blue" "+")
triple10
Harry is furry.
("Harry" "is" "furry" "+")
triple12
((triple13) -> (rule1 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
triple13
Harry is kind.
("Harry" "is" "kind" "+")
triple14
((triple15 triple12) -> (rule7 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
((triple15 ((triple13) -> (rule1 % int2))) -> (rule7 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
((((triple12) -> (rule2 % int2)) triple12) -> (rule7 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
((((triple13) -> (rule3 % int2)) triple12) -> (rule7 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
((((triple12) -> (rule2 % int3)) ((triple13) -> (rule1 % int2))) -> (rule7 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
((((triple13) -> (rule3 % int3)) ((triple13) -> (rule1 % int2))) -> (rule7 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
((((((triple13) -> (rule1 % int3))) -> (rule2 % int2)) triple12) -> (rule7 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
((((((triple13) -> (rule1 % int3))) -> (rule2 % int2)) ((triple13) -> (rule1 % int3))) -> (rule7 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
Harry is nice.
("Harry" "is" "nice" "+")
triple15
((triple12) -> (rule2 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
((triple13) -> (rule3 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
((((triple13) -> (rule1 % int2))) -> (rule2 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is not cold.
("Harry" "is" "cold" "-")
triple11
Harry is smart.
("Harry" "is" "smart" "+")
triple16
((triple14) -> (rule6 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
((((triple15 triple12) -> (rule7 % int2))) -> (rule6 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
((((triple15 ((triple13) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
((((((triple12) -> (rule2 % int3)) triple12) -> (rule7 % int2))) -> (rule6 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
((((((triple13) -> (rule3 % int3)) triple12) -> (rule7 % int2))) -> (rule6 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
((((((triple12) -> (rule2 % int4)) ((triple13) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
Harry is nice.
("Harry" "is" "nice" "+")
int4
((((((triple13) -> (rule3 % int4)) ((triple13) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
Harry is nice.
("Harry" "is" "nice" "+")
int4
((((((((triple13) -> (rule1 % int4))) -> (rule2 % int3)) triple12) -> (rule7 % int2))) -> (rule6 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Harry is furry.
("Harry" "is" "furry" "+")
int4
((((((((triple13) -> (rule1 % int4))) -> (rule2 % int3)) ((triple13) -> (rule1 % int4))) -> (rule7 % int2))) -> (rule6 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Harry is furry.
("Harry" "is" "furry" "+")
int4
Gary is nice.
("Gary" "is" "nice" "+")
((triple8) -> (rule2 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
((triple9) -> (rule3 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
((((triple9) -> (rule1 % int2))) -> (rule2 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
((((triple8) -> (rule2 % int2)) triple8) -> (rule7 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
((((triple9) -> (rule3 % int2)) triple8) -> (rule7 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
((((triple8) -> (rule2 % int3)) ((triple9) -> (rule1 % int2))) -> (rule7 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
((((triple9) -> (rule3 % int3)) ((triple9) -> (rule1 % int2))) -> (rule7 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
((((((triple9) -> (rule1 % int3))) -> (rule2 % int2)) triple8) -> (rule7 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3
((((((triple9) -> (rule1 % int3))) -> (rule2 % int2)) ((triple9) -> (rule1 % int3))) -> (rule7 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3
Gary is smart.
("Gary" "is" "smart" "+")
((((((triple8) -> (rule2 % int3)) triple8) -> (rule7 % int2))) -> (rule6 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
((((((triple9) -> (rule3 % int3)) triple8) -> (rule7 % int2))) -> (rule6 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
((((((triple8) -> (rule2 % int4)) ((triple9) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3
Gary is nice.
("Gary" "is" "nice" "+")
int4
((((((triple9) -> (rule3 % int4)) ((triple9) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3
Gary is nice.
("Gary" "is" "nice" "+")
int4
((((((((triple9) -> (rule1 % int4))) -> (rule2 % int3)) triple8) -> (rule7 % int2))) -> (rule6 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
Gary is furry.
("Gary" "is" "furry" "+")
int4
((((((((triple9) -> (rule1 % int4))) -> (rule2 % int3)) ((triple9) -> (rule1 % int4))) -> (rule7 % int2))) -> (rule6 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
Gary is furry.
("Gary" "is" "furry" "+")
int4