Dave is smart. Dave is young. Erin is cold. Gary is blue. Gary is cold. Gary is furry. Gary is kind. Gary is rough. Gary is smart. Harry is blue. Harry is furry. Harry is kind. Harry is rough. Harry is smart. Harry is young. All blue, cold things are smart. If Erin is smart and Erin is young then Erin is cold. If Erin is kind and Erin is cold then Erin is young. Young, furry things are smart. All furry things are blue. Cold things are rough. If something is rough and furry then it is blue. If something is blue and smart then it is furry.
Dave is smart.
("Dave" "is" "smart" "+")
Dave is young.
("Dave" "is" "young" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is young.
("Harry" "is" "young" "+")
All blue, cold things are smart.
((("something" "is" "blue" "+") ("something" "is" "cold" "+")) -> ("something" "is" "smart" "+"))
If Erin is smart and Erin is young then Erin is cold.
((("Erin" "is" "smart" "+") ("Erin" "is" "young" "+")) -> ("Erin" "is" "cold" "+"))
If Erin is kind and Erin is cold then Erin is young.
((("Erin" "is" "kind" "+") ("Erin" "is" "cold" "+")) -> ("Erin" "is" "young" "+"))
Young, furry things are smart.
((("something" "is" "young" "+") ("something" "is" "furry" "+")) -> ("something" "is" "smart" "+"))
All furry things are blue.
((("something" "is" "furry" "+")) -> ("something" "is" "blue" "+"))
Cold things are rough.
((("something" "is" "cold" "+")) -> ("something" "is" "rough" "+"))
If something is rough and furry then it is blue.
((("something" "is" "rough" "+") ("something" "is" "furry" "+")) -> ("something" "is" "blue" "+"))
If something is blue and smart then it is furry.
((("something" "is" "blue" "+") ("something" "is" "smart" "+")) -> ("something" "is" "furry" "+"))
Gary is smart.
True
1
proof
[(triple9 OR ((triple4 triple5) -> rule1) OR ((((triple6) -> rule5) triple5) -> rule1) OR ((((triple8 triple6) -> rule7) triple5) -> rule1) OR ((((((triple5) -> rule6) triple6) -> rule7) triple5) -> rule1))]
("Gary" "is" "smart" "+")
triple9
((triple4 triple5) -> (rule1 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
((((triple6) -> (rule5 % int2)) triple5) -> (rule1 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
((((triple8 triple6) -> (rule7 % int2)) triple5) -> (rule1 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
((((((triple5) -> (rule6 % int3)) triple6) -> (rule7 % int2)) triple5) -> (rule1 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
Harry is not furry.
False
1
inv-proof
[(triple11 OR ((triple10 triple14) -> rule8))]
("Harry" "is" "furry" "-")
triple11
((triple10 triple14) -> (rule8 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Erin is not young.
Unknown
inv-rconc
[@1: Erin is young.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Erin" "is" "young" "-")
Harry is cold.
Unknown
random
[@0: Harry is cold.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "cold" "+")
@0: Dave is smart.[(triple1)] Dave is young.[(triple2)] Erin is cold.[(triple3)] Gary is blue.[(triple4 OR ((triple6) -> rule5) OR ((triple8 triple6) -> rule7) OR ((((triple5) -> rule6) triple6) -> rule7))] Gary is cold.[(triple5)] Gary is furry.[(triple6 OR ((triple4 triple9) -> rule8) OR ((triple4 ((triple4 triple5) -> rule1)) -> rule8))] Gary is kind.[(triple7)] Gary is rough.[(triple8 OR ((triple5) -> rule6))] Gary is smart.[(triple9 OR ((triple4 triple5) -> rule1) OR ((((triple6) -> rule5) triple5) -> rule1) OR ((((triple8 triple6) -> rule7) triple5) -> rule1) OR ((((((triple5) -> rule6) triple6) -> rule7) triple5) -> rule1))] Harry is blue.[(triple10 OR ((triple11) -> rule5) OR ((triple13 triple11) -> rule7))] Harry is furry.[(triple11 OR ((triple10 triple14) -> rule8))] Harry is kind.[(triple12)] Harry is rough.[(triple13)] Harry is smart.[(triple14 OR ((triple15 triple11) -> rule4))] Harry is young.[(triple15)] @1: Erin is rough.[(((triple3) -> rule6))]
Dave is smart.
("Dave" "is" "smart" "+")
triple1
Dave is young.
("Dave" "is" "young" "+")
triple2
Erin is cold.
("Erin" "is" "cold" "+")
triple3
Gary is blue.
("Gary" "is" "blue" "+")
triple4
((triple6) -> (rule5 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
((triple8 triple6) -> (rule7 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
((((triple5) -> (rule6 % int2)) triple6) -> (rule7 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
triple5
Gary is furry.
("Gary" "is" "furry" "+")
triple6
((triple4 triple9) -> (rule8 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
((triple4 ((triple4 triple5) -> (rule1 % int2))) -> (rule8 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
triple7
Gary is rough.
("Gary" "is" "rough" "+")
triple8
((triple5) -> (rule6 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
triple9
((triple4 triple5) -> (rule1 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
((((triple6) -> (rule5 % int2)) triple5) -> (rule1 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
((((triple8 triple6) -> (rule7 % int2)) triple5) -> (rule1 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
((((((triple5) -> (rule6 % int3)) triple6) -> (rule7 % int2)) triple5) -> (rule1 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
Harry is blue.
("Harry" "is" "blue" "+")
triple10
((triple11) -> (rule5 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
((triple13 triple11) -> (rule7 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
triple11
((triple10 triple14) -> (rule8 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
triple12
Harry is rough.
("Harry" "is" "rough" "+")
triple13
Harry is smart.
("Harry" "is" "smart" "+")
triple14
((triple15 triple11) -> (rule4 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
triple15
Erin is rough.
("Erin" "is" "rough" "+")
((triple3) -> (rule6 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1