Anne is blue. Anne is green. Anne is nice. Bob is nice. Gary is big. Harry is green. Harry is nice. All cold, smart people are green. All kind people are cold. If Gary is green and Gary is big then Gary is smart. Cold, big people are smart. If Bob is nice then Bob is kind. All kind, smart people are big.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Gary is big.
("Gary" "is" "big" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is nice.
("Harry" "is" "nice" "+")
All cold, smart people are green.
((("someone" "is" "cold" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "green" "+"))
All kind people are cold.
((("someone" "is" "kind" "+")) -> ("someone" "is" "cold" "+"))
If Gary is green and Gary is big then Gary is smart.
((("Gary" "is" "green" "+") ("Gary" "is" "big" "+")) -> ("Gary" "is" "smart" "+"))
Cold, big people are smart.
((("someone" "is" "cold" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "smart" "+"))
If Bob is nice then Bob is kind.
((("Bob" "is" "nice" "+")) -> ("Bob" "is" "kind" "+"))
All kind, smart people are big.
((("someone" "is" "kind" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "big" "+"))
Gary is big.
True
1
proof
[(triple5)]
("Gary" "is" "big" "+")
triple5
Harry is not green.
False
1
inv-proof
[(triple6)]
("Harry" "is" "green" "-")
triple6
Bob is kind.
True
2
proof
[(((triple4) -> rule5))]
("Bob" "is" "kind" "+")
((triple4) -> (rule5 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is not kind.
False
2
inv-proof
[(((triple4) -> rule5))]
("Bob" "is" "kind" "-")
((triple4) -> (rule5 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is cold.
True
3
proof
[(((((triple4) -> rule5)) -> rule2))]
("Bob" "is" "cold" "+")
((((triple4) -> (rule5 % int2))) -> (rule2 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is not cold.
False
3
inv-proof
[(((((triple4) -> rule5)) -> rule2))]
("Bob" "is" "cold" "-")
((((triple4) -> (rule5 % int2))) -> (rule2 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Anne is not big.
Unknown
inv-rconc
[@1: Anne is big.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Anne" "is" "big" "-")
Bob is green.
Unknown
rconc
[@3: Bob is green.[CWA. Example of deepest failure = (rule1 <- rule4 <- rule6 <- FAIL)]]
("Bob" "is" "green" "+")
Gary is not green.
Unknown
inv-rconc
[@2: Gary is green.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("Gary" "is" "green" "-")
Anne is kind.
Unknown
random
[@0: Anne is kind.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "kind" "+")
Gary is not kind.
Unknown
inv-random
[@0: Gary is kind.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "kind" "-")
Harry is kind.
Unknown
random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "+")
@0: Anne is blue.[(triple1)] Anne is green.[(triple2)] Anne is nice.[(triple3)] Bob is nice.[(triple4)] Gary is big.[(triple5)] Harry is green.[(triple6)] Harry is nice.[(triple7)] @1: Bob is kind.[(((triple4) -> rule5))] @2: Bob is cold.[(((((triple4) -> rule5)) -> rule2))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is green.
("Anne" "is" "green" "+")
triple2
Anne is nice.
("Anne" "is" "nice" "+")
triple3
Bob is nice.
("Bob" "is" "nice" "+")
triple4
Gary is big.
("Gary" "is" "big" "+")
triple5
Harry is green.
("Harry" "is" "green" "+")
triple6
Harry is nice.
("Harry" "is" "nice" "+")
triple7
Bob is kind.
("Bob" "is" "kind" "+")
((triple4) -> (rule5 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
((((triple4) -> (rule5 % int2))) -> (rule2 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2