Anne is furry. Anne is not smart. Charlie is cold. Gary is furry. Gary is round. Gary is smart. Harry is cold. Harry is nice. Harry is not rough. Harry is round. Harry is smart. If Charlie is cold then Charlie is furry. All blue, furry things are nice. Furry, blue things are nice. Nice things are blue. If Harry is rough then Harry is cold. If something is smart and furry then it is rough. If Anne is blue then Anne is cold. If Charlie is furry then Charlie is nice. If Charlie is blue then Charlie is smart.
Anne is furry.
("Anne" "is" "furry" "+")
Anne is not smart.
("Anne" "is" "smart" "-")
Charlie is cold.
("Charlie" "is" "cold" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is not rough.
("Harry" "is" "rough" "-")
Harry is round.
("Harry" "is" "round" "+")
Harry is smart.
("Harry" "is" "smart" "+")
If Charlie is cold then Charlie is furry.
((("Charlie" "is" "cold" "+")) -> ("Charlie" "is" "furry" "+"))
All blue, furry things are nice.
((("something" "is" "blue" "+") ("something" "is" "furry" "+")) -> ("something" "is" "nice" "+"))
Furry, blue things are nice.
((("something" "is" "furry" "+") ("something" "is" "blue" "+")) -> ("something" "is" "nice" "+"))
Nice things are blue.
((("something" "is" "nice" "+")) -> ("something" "is" "blue" "+"))
If Harry is rough then Harry is cold.
((("Harry" "is" "rough" "+")) -> ("Harry" "is" "cold" "+"))
If something is smart and furry then it is rough.
((("something" "is" "smart" "+") ("something" "is" "furry" "+")) -> ("something" "is" "rough" "+"))
If Anne is blue then Anne is cold.
((("Anne" "is" "blue" "+")) -> ("Anne" "is" "cold" "+"))
If Charlie is furry then Charlie is nice.
((("Charlie" "is" "furry" "+")) -> ("Charlie" "is" "nice" "+"))
If Charlie is blue then Charlie is smart.
((("Charlie" "is" "blue" "+")) -> ("Charlie" "is" "smart" "+"))
Harry is not rough.
True
1
proof
[(triple9)]
("Harry" "is" "rough" "-")
triple9
Harry is not smart.
False
1
inv-proof
[(triple11)]
("Harry" "is" "smart" "-")
triple11
Charlie is furry.
True
2
proof
[(((triple3) -> rule1))]
("Charlie" "is" "furry" "+")
((triple3) -> (rule1 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is not furry.
False
2
inv-proof
[(((triple3) -> rule1))]
("Charlie" "is" "furry" "-")
((triple3) -> (rule1 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is nice.
True
3
proof
[(((((triple3) -> rule1)) -> rule8))]
("Charlie" "is" "nice" "+")
((((triple3) -> (rule1 % int2))) -> (rule8 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is not nice.
False
3
inv-proof
[(((((triple3) -> rule1)) -> rule8))]
("Charlie" "is" "nice" "-")
((((triple3) -> (rule1 % int2))) -> (rule8 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is blue.
True
4
proof
[(((((((triple3) -> rule1)) -> rule8)) -> rule4))]
("Charlie" "is" "blue" "+")
((((((triple3) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3
Charlie is not blue.
False
4
inv-proof
[(((((((triple3) -> rule1)) -> rule8)) -> rule4))]
("Charlie" "is" "blue" "-")
((((((triple3) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3
Charlie is smart.
True
5
proof
[(((((((((triple3) -> rule1)) -> rule8)) -> rule4)) -> rule9))]
("Charlie" "is" "smart" "+")
((((((((triple3) -> (rule1 % int4))) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule9 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Charlie is furry.
("Charlie" "is" "furry" "+")
int4
Charlie is not smart.
False
5
inv-proof
[(((((((((triple3) -> rule1)) -> rule8)) -> rule4)) -> rule9))]
("Charlie" "is" "smart" "-")
((((((((triple3) -> (rule1 % int4))) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule9 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Charlie is furry.
("Charlie" "is" "furry" "+")
int4
Charlie is rough.
True
8
proof
[(((((((((((triple3) -> rule1)) -> rule8)) -> rule4)) -> rule9) ((triple3) -> rule1)) -> rule6))]
("Charlie" "is" "rough" "+")
((((((((((triple3) -> (rule1 % int5))) -> (rule8 % int4))) -> (rule4 % int3))) -> (rule9 % int2)) ((triple3) -> (rule1 % int5))) -> (rule6 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Charlie is nice.
("Charlie" "is" "nice" "+")
int4
Charlie is furry.
("Charlie" "is" "furry" "+")
int5
Charlie is not rough.
False
8
inv-proof
[(((((((((((triple3) -> rule1)) -> rule8)) -> rule4)) -> rule9) ((triple3) -> rule1)) -> rule6))]
("Charlie" "is" "rough" "-")
((((((((((triple3) -> (rule1 % int5))) -> (rule8 % int4))) -> (rule4 % int3))) -> (rule9 % int2)) ((triple3) -> (rule1 % int5))) -> (rule6 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Charlie is nice.
("Charlie" "is" "nice" "+")
int4
Charlie is furry.
("Charlie" "is" "furry" "+")
int5
Anne is not rough.
Unknown
inv-rconc
[@1: Anne is rough.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Anne" "is" "rough" "-")
Anne is cold.
Unknown
rconc
[@3: Anne is cold.[CWA. Example of deepest failure = (rule7 <- rule4 <- rule2 <- FAIL)]]
("Anne" "is" "cold" "+")
Gary is not blue.
Unknown
inv-rconc
[@2: Gary is blue.[CWA. Example of deepest failure = (rule4 <- rule2 <- FAIL)]]
("Gary" "is" "blue" "-")
Gary is nice.
Unknown
rconc
[@3: Gary is nice.[CWA. Example of deepest failure = (rule2 <- rule4 <- rule3 <- FAIL)]]
("Gary" "is" "nice" "+")
Anne is not blue.
Unknown
inv-rconc
[@2: Anne is blue.[CWA. Example of deepest failure = (rule4 <- rule2 <- FAIL)]]
("Anne" "is" "blue" "-")
Anne is nice.
Unknown
rconc
[@3: Anne is nice.[CWA. Example of deepest failure = (rule2 <- rule4 <- rule3 <- FAIL)]]
("Anne" "is" "nice" "+")
Charlie is not round.
Unknown
inv-random
[@0: Charlie is round.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "round" "-")
Anne is round.
Unknown
random
[@0: Anne is round.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "round" "+")
Harry is not furry.
Unknown
inv-random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "-")
Gary is cold.
Unknown
random
[@0: Gary is cold.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "cold" "+")
@0: Anne is furry.[(triple1)] Anne is not smart.[(triple2)] Charlie is cold.[(triple3)] Gary is furry.[(triple4)] Gary is round.[(triple5)] Gary is smart.[(triple6)] Harry is cold.[(triple7)] Harry is nice.[(triple8)] Harry is not rough.[(triple9)] Harry is round.[(triple10)] Harry is smart.[(triple11)] @1: Charlie is furry.[(((triple3) -> rule1))] Gary is rough.[(((triple6 triple4) -> rule6))] Harry is blue.[(((triple8) -> rule4))] @2: Charlie is nice.[(((((triple3) -> rule1)) -> rule8))] @3: Charlie is blue.[(((((((triple3) -> rule1)) -> rule8)) -> rule4))] @4: Charlie is smart.[(((((((((triple3) -> rule1)) -> rule8)) -> rule4)) -> rule9))] @5: Charlie is rough.[(((((((((((triple3) -> rule1)) -> rule8)) -> rule4)) -> rule9) ((triple3) -> rule1)) -> rule6))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Anne is not smart.
("Anne" "is" "smart" "-")
triple2
Charlie is cold.
("Charlie" "is" "cold" "+")
triple3
Gary is furry.
("Gary" "is" "furry" "+")
triple4
Gary is round.
("Gary" "is" "round" "+")
triple5
Gary is smart.
("Gary" "is" "smart" "+")
triple6
Harry is cold.
("Harry" "is" "cold" "+")
triple7
Harry is nice.
("Harry" "is" "nice" "+")
triple8
Harry is not rough.
("Harry" "is" "rough" "-")
triple9
Harry is round.
("Harry" "is" "round" "+")
triple10
Harry is smart.
("Harry" "is" "smart" "+")
triple11
Charlie is furry.
("Charlie" "is" "furry" "+")
((triple3) -> (rule1 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
((triple6 triple4) -> (rule6 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
((triple8) -> (rule4 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
((((triple3) -> (rule1 % int2))) -> (rule8 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
((((((triple3) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3
Charlie is smart.
("Charlie" "is" "smart" "+")
((((((((triple3) -> (rule1 % int4))) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule9 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Charlie is furry.
("Charlie" "is" "furry" "+")
int4
Charlie is rough.
("Charlie" "is" "rough" "+")
((((((((((triple3) -> (rule1 % int5))) -> (rule8 % int4))) -> (rule4 % int3))) -> (rule9 % int2)) ((triple3) -> (rule1 % int5))) -> (rule6 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Charlie is nice.
("Charlie" "is" "nice" "+")
int4
Charlie is furry.
("Charlie" "is" "furry" "+")
int5