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