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