Bob is round. Dave is kind. Fiona is furry. Harry is kind. If something is green and round then it is quiet. Round things are white. If something is white then it is round. If something is kind and round then it is nice. Quiet things are green. Kind things are white. All kind, round things are nice. White, furry things are quiet.
Bob is round.
("Bob" "is" "round" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Harry is kind.
("Harry" "is" "kind" "+")
If something is green and round then it is quiet.
((("something" "is" "green" "+") ("something" "is" "round" "+")) -> ("something" "is" "quiet" "+"))
Round things are white.
((("something" "is" "round" "+")) -> ("something" "is" "white" "+"))
If something is white then it is round.
((("something" "is" "white" "+")) -> ("something" "is" "round" "+"))
If something is kind and round then it is nice.
((("something" "is" "kind" "+") ("something" "is" "round" "+")) -> ("something" "is" "nice" "+"))
Quiet things are green.
((("something" "is" "quiet" "+")) -> ("something" "is" "green" "+"))
Kind things are white.
((("something" "is" "kind" "+")) -> ("something" "is" "white" "+"))
All kind, round things are nice.
((("something" "is" "kind" "+") ("something" "is" "round" "+")) -> ("something" "is" "nice" "+"))
White, furry things are quiet.
((("something" "is" "white" "+") ("something" "is" "furry" "+")) -> ("something" "is" "quiet" "+"))
Dave is kind.
True
1
proof
[(triple2)]
("Dave" "is" "kind" "+")
triple2
Dave is not kind.
False
1
inv-proof
[(triple2)]
("Dave" "is" "kind" "-")
triple2
Harry is white.
True
2
proof
[(((triple4) -> rule6))]
("Harry" "is" "white" "+")
((triple4) -> (rule6 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Bob is not white.
False
2
inv-proof
[(((triple1) -> rule2))]
("Bob" "is" "white" "-")
((triple1) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Dave is round.
True
3
proof
[(((((triple2) -> rule6)) -> rule3))]
("Dave" "is" "round" "+")
((((triple2) -> (rule6 % int2))) -> (rule3 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Harry is not round.
False
3
inv-proof
[(((((triple4) -> rule6)) -> rule3))]
("Harry" "is" "round" "-")
((((triple4) -> (rule6 % int2))) -> (rule3 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Bob is not quiet.
Unknown
inv-rconc
[@3: Bob is quiet.[CWA. Example of deepest failure = (rule1 <- rule5 <- rule8 <- FAIL)]]
("Bob" "is" "quiet" "-")
Dave is green.
Unknown
rconc
[@2: Dave is green.[CWA. Example of deepest failure = (rule5 <- rule1 <- FAIL)]]
("Dave" "is" "green" "+")
Harry is not green.
Unknown
inv-rconc
[@2: Harry is green.[CWA. Example of deepest failure = (rule5 <- rule1 <- FAIL)]]
("Harry" "is" "green" "-")
Dave is furry.
Unknown
random
[@0: Dave is furry.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "furry" "+")
Fiona is not kind.
Unknown
inv-random
[@0: Fiona is kind.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "kind" "-")
Bob is furry.
Unknown
random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "+")
@0: Bob is round.[(triple1)] Dave is kind.[(triple2)] Fiona is furry.[(triple3)] Harry is kind.[(triple4)] @1: Bob is white.[(((triple1) -> rule2))] Dave is white.[(((triple2) -> rule6))] Harry is white.[(((triple4) -> rule6))] @2: Dave is round.[(((((triple2) -> rule6)) -> rule3))] Harry is round.[(((((triple4) -> rule6)) -> rule3))] @3: Dave is nice.[(((triple2 ((((triple2) -> rule6)) -> rule3)) -> rule4) OR ((triple2 ((((triple2) -> rule6)) -> rule3)) -> rule7))] Harry is nice.[(((triple4 ((((triple4) -> rule6)) -> rule3)) -> rule4) OR ((triple4 ((((triple4) -> rule6)) -> rule3)) -> rule7))]
Bob is round.
("Bob" "is" "round" "+")
triple1
Dave is kind.
("Dave" "is" "kind" "+")
triple2
Fiona is furry.
("Fiona" "is" "furry" "+")
triple3
Harry is kind.
("Harry" "is" "kind" "+")
triple4
Bob is white.
("Bob" "is" "white" "+")
((triple1) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
((triple2) -> (rule6 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
((triple4) -> (rule6 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
((((triple2) -> (rule6 % int2))) -> (rule3 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
((((triple4) -> (rule6 % int2))) -> (rule3 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
((triple2 ((((triple2) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
((triple2 ((((triple2) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Harry is nice.
("Harry" "is" "nice" "+")
((triple4 ((((triple4) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
((triple4 ((((triple4) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3