Erin is cold. Erin is white. Harry is furry. Furry things are blue. Smart, furry things are white. All rough things are cold. Furry, rough things are blue. All white things are cold. All blue things are smart. All rough things are white. All green things are smart.
Erin is cold.
("Erin" "is" "cold" "+")
Erin is white.
("Erin" "is" "white" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Furry things are blue.
((("something" "is" "furry" "+")) -> ("something" "is" "blue" "+"))
Smart, furry things are white.
((("something" "is" "smart" "+") ("something" "is" "furry" "+")) -> ("something" "is" "white" "+"))
All rough things are cold.
((("something" "is" "rough" "+")) -> ("something" "is" "cold" "+"))
Furry, rough things are blue.
((("something" "is" "furry" "+") ("something" "is" "rough" "+")) -> ("something" "is" "blue" "+"))
All white things are cold.
((("something" "is" "white" "+")) -> ("something" "is" "cold" "+"))
All blue things are smart.
((("something" "is" "blue" "+")) -> ("something" "is" "smart" "+"))
All rough things are white.
((("something" "is" "rough" "+")) -> ("something" "is" "white" "+"))
All green things are smart.
((("something" "is" "green" "+")) -> ("something" "is" "smart" "+"))
Harry is furry.
True
1
proof
[(triple3)]
("Harry" "is" "furry" "+")
triple3
Erin is not white.
False
1
inv-proof
[(triple2)]
("Erin" "is" "white" "-")
triple2
Harry is blue.
True
2
proof
[(((triple3) -> rule1))]
("Harry" "is" "blue" "+")
((triple3) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is not blue.
False
2
inv-proof
[(((triple3) -> rule1))]
("Harry" "is" "blue" "-")
((triple3) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is smart.
True
3
proof
[(((((triple3) -> rule1)) -> rule6))]
("Harry" "is" "smart" "+")
((((triple3) -> (rule1 % int2))) -> (rule6 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is not smart.
False
3
inv-proof
[(((((triple3) -> rule1)) -> rule6))]
("Harry" "is" "smart" "-")
((((triple3) -> (rule1 % int2))) -> (rule6 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Erin is not blue.
Unknown
inv-rconc
[@1: Erin is blue.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "blue" "-")
Erin is smart.
Unknown
rconc
[@2: Erin is smart.[CWA. Example of deepest failure = (rule6 <- rule1 <- FAIL)]]
("Erin" "is" "smart" "+")
Harry is not green.
Unknown
inv-random
[@0: Harry is green.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "green" "-")
Erin is rough.
Unknown
random
[@0: Erin is rough.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "rough" "+")
Harry is not rough.
Unknown
inv-random
[@0: Harry is rough.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "rough" "-")
Erin is green.
Unknown
random
[@0: Erin is green.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "green" "+")
@0: Erin is cold.[(triple1 OR ((triple2) -> rule5))] Erin is white.[(triple2)] Harry is furry.[(triple3)] @1: Harry is blue.[(((triple3) -> rule1))] @2: Harry is smart.[(((((triple3) -> rule1)) -> rule6))] @3: Harry is white.[(((((((triple3) -> rule1)) -> rule6) triple3) -> rule2))] @4: Harry is cold.[(((((((((triple3) -> rule1)) -> rule6) triple3) -> rule2)) -> rule5))]
Erin is cold.
("Erin" "is" "cold" "+")
triple1
((triple2) -> (rule5 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
triple2
Harry is furry.
("Harry" "is" "furry" "+")
triple3
Harry is blue.
("Harry" "is" "blue" "+")
((triple3) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
((((triple3) -> (rule1 % int2))) -> (rule6 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
((((((triple3) -> (rule1 % int3))) -> (rule6 % int2)) triple3) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Harry is cold.
("Harry" "is" "cold" "+")
((((((((triple3) -> (rule1 % int4))) -> (rule6 % int3)) triple3) -> (rule2 % int2))) -> (rule5 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
Harry is blue.
("Harry" "is" "blue" "+")
int4