Bob is blue. Bob is cold. Bob is red. Charlie is kind. Gary is blue. Gary is cold. Harry is smart. All smart things are kind.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is red.
("Bob" "is" "red" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Harry is smart.
("Harry" "is" "smart" "+")
All smart things are kind.
((("something" "is" "smart" "+")) -> ("something" "is" "kind" "+"))
Harry is smart.
True
1
proof
[(triple7)]
("Harry" "is" "smart" "+")
triple7
Gary is not cold.
False
1
inv-proof
[(triple6)]
("Gary" "is" "cold" "-")
triple6
Harry is kind.
True
2
proof
[(((triple7) -> rule1))]
("Harry" "is" "kind" "+")
((triple7) -> (rule1 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is not kind.
False
2
inv-proof
[(((triple7) -> rule1))]
("Harry" "is" "kind" "-")
((triple7) -> (rule1 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Gary is not kind.
Unknown
inv-rconc
[@1: Gary is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "kind" "-")
Bob is kind.
Unknown
rconc
[@1: Bob is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "kind" "+")
Harry is not cold.
Unknown
inv-random
[@0: Harry is cold.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "cold" "-")
Charlie is red.
Unknown
random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "+")
@0: Bob is blue.[(triple1)] Bob is cold.[(triple2)] Bob is red.[(triple3)] Charlie is kind.[(triple4)] Gary is blue.[(triple5)] Gary is cold.[(triple6)] Harry is smart.[(triple7)] @1: Harry is kind.[(((triple7) -> rule1))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is cold.
("Bob" "is" "cold" "+")
triple2
Bob is red.
("Bob" "is" "red" "+")
triple3
Charlie is kind.
("Charlie" "is" "kind" "+")
triple4
Gary is blue.
("Gary" "is" "blue" "+")
triple5
Gary is cold.
("Gary" "is" "cold" "+")
triple6
Harry is smart.
("Harry" "is" "smart" "+")
triple7
Harry is kind.
("Harry" "is" "kind" "+")
((triple7) -> (rule1 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1