Bob is smart. Dave is quiet. Dave is smart. Harry is blue. Harry is kind. Harry is quiet. Harry is smart. All furry people are nice. Quiet people are kind. If Bob is smart then Bob is quiet. All kind people are not furry. All kind people are quiet. Furry, nice people are quiet. If someone is kind and smart then they are white. If someone is nice and not furry then they are white.
Bob is smart.
("Bob" "is" "smart" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is smart.
("Harry" "is" "smart" "+")
All furry people are nice.
((("someone" "is" "furry" "+")) -> ("someone" "is" "nice" "+"))
Quiet people are kind.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "kind" "+"))
If Bob is smart then Bob is quiet.
((("Bob" "is" "smart" "+")) -> ("Bob" "is" "quiet" "+"))
All kind people are not furry.
((("someone" "is" "kind" "+")) -> ("someone" "is" "furry" "-"))
All kind people are quiet.
((("someone" "is" "kind" "+")) -> ("someone" "is" "quiet" "+"))
Furry, nice people are quiet.
((("someone" "is" "furry" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "quiet" "+"))
If someone is kind and smart then they are white.
((("someone" "is" "kind" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "white" "+"))
If someone is nice and not furry then they are white.
((("someone" "is" "nice" "+") ("someone" "is" "furry" "~")) -> ("someone" "is" "white" "+"))
Dave is quiet.
True
1
proof
[(triple2)]
("Dave" "is" "quiet" "+")
triple2
Harry is not smart.
False
1
inv-proof
[(triple7)]
("Harry" "is" "smart" "-")
triple7
Bob is quiet.
True
2
proof
[(((triple1) -> rule3))]
("Bob" "is" "quiet" "+")
((triple1) -> (rule3 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Dave is not kind.
False
2
inv-proof
[(((triple2) -> rule2))]
("Dave" "is" "kind" "-")
((triple2) -> (rule2 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is white.
True
4
proof
[(((((triple2) -> rule2) triple3) -> rule7))]
("Dave" "is" "white" "+")
((((triple2) -> (rule2 % int2)) triple3) -> (rule7 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is furry.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule4))]
("Dave" "is" "furry" "+")
((((triple2) -> (rule2 % int2))) -> (rule4 % int1))
Dave is not furry.
("Dave" "is" "furry" "-")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Bob is white.
True
5
proof
[(((((((triple1) -> rule3)) -> rule2) triple1) -> rule7))]
("Bob" "is" "white" "+")
((((((triple1) -> (rule3 % int3))) -> (rule2 % int2)) triple1) -> (rule7 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Bob is not white.
False
5
inv-proof
[(((((((triple1) -> rule3)) -> rule2) triple1) -> rule7))]
("Bob" "is" "white" "-")
((((((triple1) -> (rule3 % int3))) -> (rule2 % int2)) triple1) -> (rule7 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Dave is not nice.
Unknown
inv-rconc
[@1: Dave is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "nice" "-")
Bob is nice.
Unknown
rconc
[@1: Bob is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "nice" "+")
Harry is not nice.
Unknown
inv-rconc
[@1: Harry is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "nice" "-")
Bob is blue.
Unknown
random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "+")
@0: Bob is smart.[(triple1)] Dave is quiet.[(triple2)] Dave is smart.[(triple3)] Harry is blue.[(triple4)] Harry is kind.[(triple5 OR ((triple6) -> rule2))] Harry is quiet.[(triple6 OR ((triple5) -> rule5))] Harry is smart.[(triple7)] @1: Bob is quiet.[(((triple1) -> rule3))] Dave is kind.[(((triple2) -> rule2))] Harry is not furry.[(((triple5) -> rule4) OR ((((triple6) -> rule2)) -> rule4))] Harry is white.[(((triple5 triple7) -> rule7) OR ((((triple6) -> rule2) triple7) -> rule7))] @2: Bob is kind.[(((((triple1) -> rule3)) -> rule2))] Dave is not furry.[(((((triple2) -> rule2)) -> rule4))] Dave is white.[(((((triple2) -> rule2) triple3) -> rule7))] @3: Bob is not furry.[(((((((triple1) -> rule3)) -> rule2)) -> rule4))] Bob is white.[(((((((triple1) -> rule3)) -> rule2) triple1) -> rule7))]
Bob is smart.
("Bob" "is" "smart" "+")
triple1
Dave is quiet.
("Dave" "is" "quiet" "+")
triple2
Dave is smart.
("Dave" "is" "smart" "+")
triple3
Harry is blue.
("Harry" "is" "blue" "+")
triple4
Harry is kind.
("Harry" "is" "kind" "+")
triple5
((triple6) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
triple6
((triple5) -> (rule5 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
triple7
Bob is quiet.
("Bob" "is" "quiet" "+")
((triple1) -> (rule3 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
((triple2) -> (rule2 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Harry is not furry.
("Harry" "is" "furry" "-")
((triple5) -> (rule4 % int1))
Harry is not furry.
("Harry" "is" "furry" "-")
int1
((((triple6) -> (rule2 % int2))) -> (rule4 % int1))
Harry is not furry.
("Harry" "is" "furry" "-")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
((triple5 triple7) -> (rule7 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
((((triple6) -> (rule2 % int2)) triple7) -> (rule7 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Dave is not furry.
("Dave" "is" "furry" "-")
((((triple2) -> (rule2 % int2))) -> (rule4 % int1))
Dave is not furry.
("Dave" "is" "furry" "-")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
((((triple2) -> (rule2 % int2)) triple3) -> (rule7 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Bob is not furry.
("Bob" "is" "furry" "-")
((((((triple1) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Bob is not furry.
("Bob" "is" "furry" "-")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
((((((triple1) -> (rule3 % int3))) -> (rule2 % int2)) triple1) -> (rule7 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3