Anne is cold. Anne is green. Anne is not kind. Anne is nice. Anne is not rough. Anne is round. Anne is not smart. Bob is not green. Bob is nice. Bob is rough. Bob is round. Bob is smart. Gary is not cold. Gary is nice. Gary is rough. Gary is round. If someone is smart and cold then they are round. If someone is green and kind then they are rough. Cold people are nice. All smart people are nice. All kind people are smart. All kind people are smart. If Anne is rough and Anne is not kind then Anne is round. Smart people are cold.
Anne is cold.
("Anne" "is" "cold" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is not kind.
("Anne" "is" "kind" "-")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is not rough.
("Anne" "is" "rough" "-")
Anne is round.
("Anne" "is" "round" "+")
Anne is not smart.
("Anne" "is" "smart" "-")
Bob is not green.
("Bob" "is" "green" "-")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Gary is not cold.
("Gary" "is" "cold" "-")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is round.
("Gary" "is" "round" "+")
If someone is smart and cold then they are round.
((("someone" "is" "smart" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "round" "+"))
If someone is green and kind then they are rough.
((("someone" "is" "green" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "rough" "+"))
Cold people are nice.
((("someone" "is" "cold" "+")) -> ("someone" "is" "nice" "+"))
All smart people are nice.
((("someone" "is" "smart" "+")) -> ("someone" "is" "nice" "+"))
All kind people are smart.
((("someone" "is" "kind" "+")) -> ("someone" "is" "smart" "+"))
All kind people are smart.
((("someone" "is" "kind" "+")) -> ("someone" "is" "smart" "+"))
If Anne is rough and Anne is not kind then Anne is round.
((("Anne" "is" "rough" "+") ("Anne" "is" "kind" "~")) -> ("Anne" "is" "round" "+"))
Smart people are cold.
((("someone" "is" "smart" "+")) -> ("someone" "is" "cold" "+"))
Anne is nice.
True
1
proof
[(triple4 OR ((triple1) -> rule3))]
("Anne" "is" "nice" "+")
triple4
((triple1) -> (rule3 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is kind.
False
1
inv-proof
[(triple3)]
("Anne" "is" "kind" "+")
triple3
Bob is cold.
True
2
proof
[(((triple12) -> rule8))]
("Bob" "is" "cold" "+")
((triple12) -> (rule8 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is not cold.
False
2
inv-proof
[(((triple12) -> rule8))]
("Bob" "is" "cold" "-")
((triple12) -> (rule8 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Gary is not smart.
Unknown
inv-rconc
[@1: Gary is smart.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Gary" "is" "smart" "-")
Gary is green.
Unknown
random
[@0: Gary is green.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "green" "+")
Bob is not kind.
Unknown
inv-random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "-")
Gary is kind.
Unknown
random
[@0: Gary is kind.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "kind" "+")
@0: Anne is cold.[(triple1)] Anne is green.[(triple2)] Anne is nice.[(triple4 OR ((triple1) -> rule3))] Anne is not kind.[(triple3)] Anne is not rough.[(triple5)] Anne is not smart.[(triple7)] Anne is round.[(triple6)] Bob is nice.[(triple9 OR ((triple12) -> rule4) OR ((((triple12) -> rule8)) -> rule3))] Bob is not green.[(triple8)] Bob is rough.[(triple10)] Bob is round.[(triple11 OR ((triple12 ((triple12) -> rule8)) -> rule1))] Bob is smart.[(triple12)] Gary is nice.[(triple14)] Gary is not cold.[(triple13)] Gary is rough.[(triple15)] Gary is round.[(triple16)] @1: Bob is cold.[(((triple12) -> rule8))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Anne is green.
("Anne" "is" "green" "+")
triple2
Anne is nice.
("Anne" "is" "nice" "+")
triple4
((triple1) -> (rule3 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is not kind.
("Anne" "is" "kind" "-")
triple3
Anne is not rough.
("Anne" "is" "rough" "-")
triple5
Anne is not smart.
("Anne" "is" "smart" "-")
triple7
Anne is round.
("Anne" "is" "round" "+")
triple6
Bob is nice.
("Bob" "is" "nice" "+")
triple9
((triple12) -> (rule4 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
((((triple12) -> (rule8 % int2))) -> (rule3 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is not green.
("Bob" "is" "green" "-")
triple8
Bob is rough.
("Bob" "is" "rough" "+")
triple10
Bob is round.
("Bob" "is" "round" "+")
triple11
((triple12 ((triple12) -> (rule8 % int2))) -> (rule1 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
triple12
Gary is nice.
("Gary" "is" "nice" "+")
triple14
Gary is not cold.
("Gary" "is" "cold" "-")
triple13
Gary is rough.
("Gary" "is" "rough" "+")
triple15
Gary is round.
("Gary" "is" "round" "+")
triple16
Bob is cold.
("Bob" "is" "cold" "+")
((triple12) -> (rule8 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1