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