Bob is cold. Bob is round. Bob is white. Charlie is cold. Charlie is green. Dave is furry. Dave is green. Dave is nice. Dave is round. Harry is furry. Harry is green. Harry is nice. Harry is round. Harry is white. If Bob is round then Bob is white. Cold, nice things are white. If something is white then it is round. All quiet things are nice. If Charlie is round and Charlie is green then Charlie is furry. Nice things are green. Cold, green things are quiet. All furry things are quiet.
Bob is cold.
("Bob" "is" "cold" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is white.
("Bob" "is" "white" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is round.
("Dave" "is" "round" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is white.
("Harry" "is" "white" "+")
If Bob is round then Bob is white.
((("Bob" "is" "round" "+")) -> ("Bob" "is" "white" "+"))
Cold, nice things are white.
((("something" "is" "cold" "+") ("something" "is" "nice" "+")) -> ("something" "is" "white" "+"))
If something is white then it is round.
((("something" "is" "white" "+")) -> ("something" "is" "round" "+"))
All quiet things are nice.
((("something" "is" "quiet" "+")) -> ("something" "is" "nice" "+"))
If Charlie is round and Charlie is green then Charlie is furry.
((("Charlie" "is" "round" "+") ("Charlie" "is" "green" "+")) -> ("Charlie" "is" "furry" "+"))
Nice things are green.
((("something" "is" "nice" "+")) -> ("something" "is" "green" "+"))
Cold, green things are quiet.
((("something" "is" "cold" "+") ("something" "is" "green" "+")) -> ("something" "is" "quiet" "+"))
All furry things are quiet.
((("something" "is" "furry" "+")) -> ("something" "is" "quiet" "+"))
Dave is nice.
True
1
proof
[(triple8 OR ((((triple6) -> rule8)) -> rule4))]
("Dave" "is" "nice" "+")
triple8
((((triple6) -> (rule8 % int2))) -> (rule4 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Bob is not white.
False
1
inv-proof
[(triple3 OR ((triple2) -> rule1))]
("Bob" "is" "white" "-")
triple3
((triple2) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Charlie is quiet.
True
3
proof
[(((triple4 triple5) -> rule7))]
("Charlie" "is" "quiet" "+")
((triple4 triple5) -> (rule7 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Harry is not quiet.
False
2
inv-proof
[(((triple10) -> rule8))]
("Harry" "is" "quiet" "-")
((triple10) -> (rule8 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Charlie is nice.
True
4
proof
[(((((triple4 triple5) -> rule7)) -> rule4))]
("Charlie" "is" "nice" "+")
((((triple4 triple5) -> (rule7 % int2))) -> (rule4 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is not nice.
False
4
inv-proof
[(((((triple4 triple5) -> rule7)) -> rule4))]
("Charlie" "is" "nice" "-")
((((triple4 triple5) -> (rule7 % int2))) -> (rule4 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is white.
True
6
proof
[(((triple4 ((((triple4 triple5) -> rule7)) -> rule4)) -> rule2))]
("Charlie" "is" "white" "+")
((triple4 ((((triple4 triple5) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
Charlie is not white.
False
6
inv-proof
[(((triple4 ((((triple4 triple5) -> rule7)) -> rule4)) -> rule2))]
("Charlie" "is" "white" "-")
((triple4 ((((triple4 triple5) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
Charlie is round.
True
7
proof
[(((((triple4 ((((triple4 triple5) -> rule7)) -> rule4)) -> rule2)) -> rule3))]
("Charlie" "is" "round" "+")
((((triple4 ((((triple4 triple5) -> (rule7 % int4))) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int4
Charlie is not round.
False
7
inv-proof
[(((((triple4 ((((triple4 triple5) -> rule7)) -> rule4)) -> rule2)) -> rule3))]
("Charlie" "is" "round" "-")
((((triple4 ((((triple4 triple5) -> (rule7 % int4))) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int4
Charlie is furry.
True
9
proof
[(((((((triple4 ((((triple4 triple5) -> rule7)) -> rule4)) -> rule2)) -> rule3) triple5) -> rule5))]
("Charlie" "is" "furry" "+")
((((((triple4 ((((triple4 triple5) -> (rule7 % int5))) -> (rule4 % int4))) -> (rule2 % int3))) -> (rule3 % int2)) triple5) -> (rule5 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
Charlie is nice.
("Charlie" "is" "nice" "+")
int4
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int5
Charlie is not furry.
False
9
inv-proof
[(((((((triple4 ((((triple4 triple5) -> rule7)) -> rule4)) -> rule2)) -> rule3) triple5) -> rule5))]
("Charlie" "is" "furry" "-")
((((((triple4 ((((triple4 triple5) -> (rule7 % int5))) -> (rule4 % int4))) -> (rule2 % int3))) -> (rule3 % int2)) triple5) -> (rule5 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
Charlie is nice.
("Charlie" "is" "nice" "+")
int4
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int5
Dave is not white.
Unknown
inv-rconc
[@1: Dave is white.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "white" "-")
Bob is green.
Unknown
rconc
[@3: Bob is green.[CWA. Example of deepest failure = (rule6 <- rule4 <- rule7 <- FAIL)]]
("Bob" "is" "green" "+")
Bob is not nice.
Unknown
inv-rconc
[@3: Bob is nice.[CWA. Example of deepest failure = (rule4 <- rule7 <- rule6 <- FAIL)]]
("Bob" "is" "nice" "-")
Bob is quiet.
Unknown
rconc
[@4: Bob is quiet.[CWA. Example of deepest failure = (rule7 <- rule6 <- rule4 <- rule8 <- FAIL)]]
("Bob" "is" "quiet" "+")
Harry is not cold.
Unknown
inv-random
[@0: Harry is cold.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "cold" "-")
Bob is furry.
Unknown
random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "+")
@0: Bob is cold.[(triple1)] Bob is round.[(triple2 OR ((triple3) -> rule3))] Bob is white.[(triple3 OR ((triple2) -> rule1))] Charlie is cold.[(triple4)] Charlie is green.[(triple5)] Dave is furry.[(triple6)] Dave is green.[(triple7 OR ((triple8) -> rule6) OR ((((((triple6) -> rule8)) -> rule4)) -> rule6))] Dave is nice.[(triple8 OR ((((triple6) -> rule8)) -> rule4))] Dave is round.[(triple9)] Harry is furry.[(triple10)] Harry is green.[(triple11 OR ((triple12) -> rule6) OR ((((((triple10) -> rule8)) -> rule4)) -> rule6))] Harry is nice.[(triple12 OR ((((triple10) -> rule8)) -> rule4))] Harry is round.[(triple13 OR ((triple14) -> rule3))] Harry is white.[(triple14)] @1: Charlie is quiet.[(((triple4 triple5) -> rule7))] Dave is quiet.[(((triple6) -> rule8))] Harry is quiet.[(((triple10) -> rule8))] @2: Charlie is nice.[(((((triple4 triple5) -> rule7)) -> rule4))] @3: Charlie is white.[(((triple4 ((((triple4 triple5) -> rule7)) -> rule4)) -> rule2))] @4: Charlie is round.[(((((triple4 ((((triple4 triple5) -> rule7)) -> rule4)) -> rule2)) -> rule3))] @5: Charlie is furry.[(((((((triple4 ((((triple4 triple5) -> rule7)) -> rule4)) -> rule2)) -> rule3) triple5) -> rule5))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
Bob is round.
("Bob" "is" "round" "+")
triple2
((triple3) -> (rule3 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
triple3
((triple2) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
triple4
Charlie is green.
("Charlie" "is" "green" "+")
triple5
Dave is furry.
("Dave" "is" "furry" "+")
triple6
Dave is green.
("Dave" "is" "green" "+")
triple7
((triple8) -> (rule6 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
((((((triple6) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Dave is nice.
("Dave" "is" "nice" "+")
triple8
((((triple6) -> (rule8 % int2))) -> (rule4 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
triple9
Harry is furry.
("Harry" "is" "furry" "+")
triple10
Harry is green.
("Harry" "is" "green" "+")
triple11
((triple12) -> (rule6 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
((((((triple10) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
Harry is nice.
("Harry" "is" "nice" "+")
triple12
((((triple10) -> (rule8 % int2))) -> (rule4 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
triple13
((triple14) -> (rule3 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
triple14
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((triple4 triple5) -> (rule7 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
((triple6) -> (rule8 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple10) -> (rule8 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
((((triple4 triple5) -> (rule7 % int2))) -> (rule4 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
((triple4 ((((triple4 triple5) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
Charlie is round.
("Charlie" "is" "round" "+")
((((triple4 ((((triple4 triple5) -> (rule7 % int4))) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int4
Charlie is furry.
("Charlie" "is" "furry" "+")
((((((triple4 ((((triple4 triple5) -> (rule7 % int5))) -> (rule4 % int4))) -> (rule2 % int3))) -> (rule3 % int2)) triple5) -> (rule5 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
Charlie is nice.
("Charlie" "is" "nice" "+")
int4
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int5