Bob is cold. Charlie is cold. Charlie is furry. Charlie is nice. Charlie is rough. Erin is rough. Harry is round. All rough things are nice. All rough things are kind. All furry things are cold. All nice, furry things are cold. Nice things are round. If something is green then it is round. Green, furry things are rough. If Harry is cold then Harry is green. If something is round then it is furry.
Bob is cold.
("Bob" "is" "cold" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Harry is round.
("Harry" "is" "round" "+")
All rough things are nice.
((("something" "is" "rough" "+")) -> ("something" "is" "nice" "+"))
All rough things are kind.
((("something" "is" "rough" "+")) -> ("something" "is" "kind" "+"))
All furry things are cold.
((("something" "is" "furry" "+")) -> ("something" "is" "cold" "+"))
All nice, furry things are cold.
((("something" "is" "nice" "+") ("something" "is" "furry" "+")) -> ("something" "is" "cold" "+"))
Nice things are round.
((("something" "is" "nice" "+")) -> ("something" "is" "round" "+"))
If something is green then it is round.
((("something" "is" "green" "+")) -> ("something" "is" "round" "+"))
Green, furry things are rough.
((("something" "is" "green" "+") ("something" "is" "furry" "+")) -> ("something" "is" "rough" "+"))
If Harry is cold then Harry is green.
((("Harry" "is" "cold" "+")) -> ("Harry" "is" "green" "+"))
If something is round then it is furry.
((("something" "is" "round" "+")) -> ("something" "is" "furry" "+"))
Charlie is nice.
True
1
proof
[(triple4 OR ((triple5) -> rule1))]
("Charlie" "is" "nice" "+")
triple4
((triple5) -> (rule1 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is not nice.
False
1
inv-proof
[(triple4 OR ((triple5) -> rule1))]
("Charlie" "is" "nice" "-")
triple4
((triple5) -> (rule1 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Harry is furry.
True
2
proof
[(((triple7) -> rule9))]
("Harry" "is" "furry" "+")
((triple7) -> (rule9 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Erin is not nice.
False
2
inv-proof
[(((triple6) -> rule1))]
("Erin" "is" "nice" "-")
((triple6) -> (rule1 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is round.
True
3
proof
[(((((triple6) -> rule1)) -> rule5))]
("Erin" "is" "round" "+")
((((triple6) -> (rule1 % int2))) -> (rule5 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is not round.
False
3
inv-proof
[(((((triple6) -> rule1)) -> rule5))]
("Erin" "is" "round" "-")
((((triple6) -> (rule1 % int2))) -> (rule5 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is furry.
True
4
proof
[(((((((triple6) -> rule1)) -> rule5)) -> rule9))]
("Erin" "is" "furry" "+")
((((((triple6) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule9 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
int3
Erin is not furry.
False
4
inv-proof
[(((((((triple6) -> rule1)) -> rule5)) -> rule9))]
("Erin" "is" "furry" "-")
((((((triple6) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule9 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
int3
Erin is cold.
True
5
proof
[(((((((((triple6) -> rule1)) -> rule5)) -> rule9)) -> rule3) OR ((((triple6) -> rule1) ((((((triple6) -> rule1)) -> rule5)) -> rule9)) -> rule4))]
("Erin" "is" "cold" "+")
((((((((triple6) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule9 % int2))) -> (rule3 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
Erin is nice.
("Erin" "is" "nice" "+")
int4
((((triple6) -> (rule1 % int4)) ((((((triple6) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule9 % int2))) -> (rule4 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
Erin is nice.
("Erin" "is" "nice" "+")
int4
Harry is not rough.
False
7
inv-proof
[(((((((((triple7) -> rule9)) -> rule3)) -> rule8) ((triple7) -> rule9)) -> rule7))]
("Harry" "is" "rough" "-")
((((((((triple7) -> (rule9 % int4))) -> (rule3 % int3))) -> (rule8 % int2)) ((triple7) -> (rule9 % int4))) -> (rule7 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Harry is furry.
("Harry" "is" "furry" "+")
int4
Harry is kind.
True
8
proof
[(((((((((((triple7) -> rule9)) -> rule3)) -> rule8) ((triple7) -> rule9)) -> rule7)) -> rule2))]
("Harry" "is" "kind" "+")
((((((((((triple7) -> (rule9 % int5))) -> (rule3 % int4))) -> (rule8 % int3)) ((triple7) -> (rule9 % int5))) -> (rule7 % int2))) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
Harry is cold.
("Harry" "is" "cold" "+")
int4
Harry is furry.
("Harry" "is" "furry" "+")
int5
Harry is not kind.
False
8
inv-proof
[(((((((((((triple7) -> rule9)) -> rule3)) -> rule8) ((triple7) -> rule9)) -> rule7)) -> rule2))]
("Harry" "is" "kind" "-")
((((((((((triple7) -> (rule9 % int5))) -> (rule3 % int4))) -> (rule8 % int3)) ((triple7) -> (rule9 % int5))) -> (rule7 % int2))) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
Harry is cold.
("Harry" "is" "cold" "+")
int4
Harry is furry.
("Harry" "is" "furry" "+")
int5
Bob is not nice.
Unknown
inv-rconc
[@2: Bob is nice.[CWA. Example of deepest failure = (rule1 <- rule7 <- FAIL)]]
("Bob" "is" "nice" "-")
Bob is furry.
Unknown
rconc
[@4: Bob is furry.[CWA. Example of deepest failure = (rule9 <- rule5 <- rule1 <- rule7 <- FAIL)]]
("Bob" "is" "furry" "+")
Bob is not rough.
Unknown
inv-rconc
[@1: Bob is rough.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Bob" "is" "rough" "-")
Bob is round.
Unknown
rconc
[@3: Bob is round.[CWA. Example of deepest failure = (rule5 <- rule1 <- rule7 <- FAIL)]]
("Bob" "is" "round" "+")
Bob is not kind.
Unknown
inv-rconc
[@2: Bob is kind.[CWA. Example of deepest failure = (rule2 <- rule7 <- FAIL)]]
("Bob" "is" "kind" "-")
Erin is green.
Unknown
random
[@0: Erin is green.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "green" "+")
Bob is not green.
Unknown
inv-random
[@0: Bob is green.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "green" "-")
Charlie is green.
Unknown
random
[@0: Charlie is green.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "green" "+")
@0: Bob is cold.[(triple1)] Charlie is cold.[(triple2 OR ((triple3) -> rule3) OR ((triple4 triple3) -> rule4) OR ((((triple5) -> rule1) triple3) -> rule4) OR ((((((triple4) -> rule5)) -> rule9)) -> rule3) OR ((triple4 ((((triple4) -> rule5)) -> rule9)) -> rule4) OR ((((triple5) -> rule1) ((((triple4) -> rule5)) -> rule9)) -> rule4) OR ((((((((triple5) -> rule1)) -> rule5)) -> rule9)) -> rule3) OR ((triple4 ((((((triple5) -> rule1)) -> rule5)) -> rule9)) -> rule4) OR ((((triple5) -> rule1) ((((((triple5) -> rule1)) -> rule5)) -> rule9)) -> rule4))] Charlie is furry.[(triple3 OR ((((triple4) -> rule5)) -> rule9) OR ((((((triple5) -> rule1)) -> rule5)) -> rule9))] Charlie is nice.[(triple4 OR ((triple5) -> rule1))] Charlie is rough.[(triple5)] Erin is rough.[(triple6)] Harry is round.[(triple7)] @1: Charlie is kind.[(((triple5) -> rule2))] Charlie is round.[(((triple4) -> rule5) OR ((((triple5) -> rule1)) -> rule5))] Erin is kind.[(((triple6) -> rule2))] Erin is nice.[(((triple6) -> rule1))] Harry is furry.[(((triple7) -> rule9))] @2: Erin is round.[(((((triple6) -> rule1)) -> rule5))] Harry is cold.[(((((triple7) -> rule9)) -> rule3))] @3: Erin is furry.[(((((((triple6) -> rule1)) -> rule5)) -> rule9))] Harry is green.[(((((((triple7) -> rule9)) -> rule3)) -> rule8))] @4: Erin is cold.[(((((((((triple6) -> rule1)) -> rule5)) -> rule9)) -> rule3) OR ((((triple6) -> rule1) ((((((triple6) -> rule1)) -> rule5)) -> rule9)) -> rule4))] Harry is rough.[(((((((((triple7) -> rule9)) -> rule3)) -> rule8) ((triple7) -> rule9)) -> rule7))] @5: Harry is kind.[(((((((((((triple7) -> rule9)) -> rule3)) -> rule8) ((triple7) -> rule9)) -> rule7)) -> rule2))] Harry is nice.[(((((((((((triple7) -> rule9)) -> rule3)) -> rule8) ((triple7) -> rule9)) -> rule7)) -> rule1))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
Charlie is cold.
("Charlie" "is" "cold" "+")
triple2
((triple3) -> (rule3 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
((triple4 triple3) -> (rule4 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
((((triple5) -> (rule1 % int2)) triple3) -> (rule4 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
((((((triple4) -> (rule5 % int3))) -> (rule9 % int2))) -> (rule3 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
((triple4 ((((triple4) -> (rule5 % int3))) -> (rule9 % int2))) -> (rule4 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
((((triple5) -> (rule1 % int4)) ((((triple4) -> (rule5 % int3))) -> (rule9 % int2))) -> (rule4 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
Charlie is nice.
("Charlie" "is" "nice" "+")
int4
((((((((triple5) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule9 % int2))) -> (rule3 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
Charlie is nice.
("Charlie" "is" "nice" "+")
int4
((triple4 ((((((triple5) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule9 % int2))) -> (rule4 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
Charlie is nice.
("Charlie" "is" "nice" "+")
int4
((((triple5) -> (rule1 % int4)) ((((((triple5) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule9 % int2))) -> (rule4 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
Charlie is nice.
("Charlie" "is" "nice" "+")
int4
Charlie is furry.
("Charlie" "is" "furry" "+")
triple3
((((triple4) -> (rule5 % int2))) -> (rule9 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
((((((triple5) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule9 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Charlie is nice.
("Charlie" "is" "nice" "+")
triple4
((triple5) -> (rule1 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
triple5
Erin is rough.
("Erin" "is" "rough" "+")
triple6
Harry is round.
("Harry" "is" "round" "+")
triple7
Charlie is kind.
("Charlie" "is" "kind" "+")
((triple5) -> (rule2 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
((triple4) -> (rule5 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
((((triple5) -> (rule1 % int2))) -> (rule5 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
((triple6) -> (rule2 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
((triple6) -> (rule1 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
((triple7) -> (rule9 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
((((triple6) -> (rule1 % int2))) -> (rule5 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
((((triple7) -> (rule9 % int2))) -> (rule3 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
((((((triple6) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule9 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
int3
Harry is green.
("Harry" "is" "green" "+")
((((((triple7) -> (rule9 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
Erin is cold.
("Erin" "is" "cold" "+")
((((((((triple6) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule9 % int2))) -> (rule3 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
Erin is nice.
("Erin" "is" "nice" "+")
int4
((((triple6) -> (rule1 % int4)) ((((((triple6) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule9 % int2))) -> (rule4 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
Erin is nice.
("Erin" "is" "nice" "+")
int4
Harry is rough.
("Harry" "is" "rough" "+")
((((((((triple7) -> (rule9 % int4))) -> (rule3 % int3))) -> (rule8 % int2)) ((triple7) -> (rule9 % int4))) -> (rule7 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Harry is furry.
("Harry" "is" "furry" "+")
int4
Harry is kind.
("Harry" "is" "kind" "+")
((((((((((triple7) -> (rule9 % int5))) -> (rule3 % int4))) -> (rule8 % int3)) ((triple7) -> (rule9 % int5))) -> (rule7 % int2))) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
Harry is cold.
("Harry" "is" "cold" "+")
int4
Harry is furry.
("Harry" "is" "furry" "+")
int5
Harry is nice.
("Harry" "is" "nice" "+")
((((((((((triple7) -> (rule9 % int5))) -> (rule3 % int4))) -> (rule8 % int3)) ((triple7) -> (rule9 % int5))) -> (rule7 % int2))) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
Harry is cold.
("Harry" "is" "cold" "+")
int4
Harry is furry.
("Harry" "is" "furry" "+")
int5