Bob is not cold. Bob is nice. Bob is quiet. Bob is rough. Bob is round. Bob is white. Dave is not blue. Dave is cold. Dave is nice. Dave is not quiet. Dave is white. Harry is not nice. Harry is rough. Harry is round. Harry is white. If someone is cold then they are rough. All white, round people are rough. If someone is round then they are rough. If someone is cold and round then they are blue. All cold people are nice. If Harry is rough and Harry is not round then Harry is cold. If someone is rough and not nice then they are quiet. All round people are quiet.
Bob is not cold.
("Bob" "is" "cold" "-")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is white.
("Bob" "is" "white" "+")
Dave is not blue.
("Dave" "is" "blue" "-")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is not quiet.
("Dave" "is" "quiet" "-")
Dave is white.
("Dave" "is" "white" "+")
Harry is not nice.
("Harry" "is" "nice" "-")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is white.
("Harry" "is" "white" "+")
If someone is cold then they are rough.
((("someone" "is" "cold" "+")) -> ("someone" "is" "rough" "+"))
All white, round people are rough.
((("someone" "is" "white" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "rough" "+"))
If someone is round then they are rough.
((("someone" "is" "round" "+")) -> ("someone" "is" "rough" "+"))
If someone is cold and round then they are blue.
((("someone" "is" "cold" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "blue" "+"))
All cold people are nice.
((("someone" "is" "cold" "+")) -> ("someone" "is" "nice" "+"))
If Harry is rough and Harry is not round then Harry is cold.
((("Harry" "is" "rough" "+") ("Harry" "is" "round" "~")) -> ("Harry" "is" "cold" "+"))
If someone is rough and not nice then they are quiet.
((("someone" "is" "rough" "+") ("someone" "is" "nice" "~")) -> ("someone" "is" "quiet" "+"))
All round people are quiet.
((("someone" "is" "round" "+")) -> ("someone" "is" "quiet" "+"))
Harry is white.
True
1
proof
[(triple15)]
("Harry" "is" "white" "+")
triple15
Bob is not round.
False
1
inv-proof
[(triple5)]
("Bob" "is" "round" "-")
triple5
Dave is rough.
True
2
proof
[(((triple8) -> rule1))]
("Dave" "is" "rough" "+")
((triple8) -> (rule1 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Harry is not quiet.
False
2
inv-proof
[(((triple14) -> rule8) OR ((triple13 triple12) -> rule7) OR ((((triple14) -> rule3) triple12) -> rule7) OR ((((triple15 triple14) -> rule2) triple12) -> rule7))]
("Harry" "is" "quiet" "-")
((triple14) -> (rule8 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
((triple13 triple12) -> (rule7 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
((((triple14) -> (rule3 % int2)) triple12) -> (rule7 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
((((triple15 triple14) -> (rule2 % int2)) triple12) -> (rule7 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Bob is not blue.
Unknown
inv-rconc
[@1: Bob is blue.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Bob" "is" "blue" "-")
Harry is cold.
Unknown
rconc
[@1: Harry is cold.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Harry" "is" "cold" "+")
@0: Bob is nice.[(triple2)] Bob is not cold.[(triple1)] Bob is quiet.[(triple3 OR ((triple5) -> rule8))] Bob is rough.[(triple4 OR ((triple5) -> rule3) OR ((triple6 triple5) -> rule2))] Bob is round.[(triple5)] Bob is white.[(triple6)] Dave is cold.[(triple8)] Dave is nice.[(triple9 OR ((triple8) -> rule5))] Dave is not blue.[(triple7)] Dave is not quiet.[(triple10)] Dave is white.[(triple11)] Harry is not nice.[(triple12)] Harry is rough.[(triple13 OR ((triple14) -> rule3) OR ((triple15 triple14) -> rule2))] Harry is round.[(triple14)] Harry is white.[(triple15)] @1: Dave is rough.[(((triple8) -> rule1))] Harry is quiet.[(((triple14) -> rule8) OR ((triple13 triple12) -> rule7) OR ((((triple14) -> rule3) triple12) -> rule7) OR ((((triple15 triple14) -> rule2) triple12) -> rule7))]
Bob is nice.
("Bob" "is" "nice" "+")
triple2
Bob is not cold.
("Bob" "is" "cold" "-")
triple1
Bob is quiet.
("Bob" "is" "quiet" "+")
triple3
((triple5) -> (rule8 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
triple4
((triple5) -> (rule3 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
((triple6 triple5) -> (rule2 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
triple5
Bob is white.
("Bob" "is" "white" "+")
triple6
Dave is cold.
("Dave" "is" "cold" "+")
triple8
Dave is nice.
("Dave" "is" "nice" "+")
triple9
((triple8) -> (rule5 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is not blue.
("Dave" "is" "blue" "-")
triple7
Dave is not quiet.
("Dave" "is" "quiet" "-")
triple10
Dave is white.
("Dave" "is" "white" "+")
triple11
Harry is not nice.
("Harry" "is" "nice" "-")
triple12
Harry is rough.
("Harry" "is" "rough" "+")
triple13
((triple14) -> (rule3 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
((triple15 triple14) -> (rule2 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
triple14
Harry is white.
("Harry" "is" "white" "+")
triple15
Dave is rough.
("Dave" "is" "rough" "+")
((triple8) -> (rule1 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple14) -> (rule8 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
((triple13 triple12) -> (rule7 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
((((triple14) -> (rule3 % int2)) triple12) -> (rule7 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
((((triple15 triple14) -> (rule2 % int2)) triple12) -> (rule7 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2