Bob is green. Gary is big. If something is green and not blue then it is not young. All blue, cold things are smart. Green things are cold. All nice things are big. If Bob is blue and Bob is not cold then Bob is smart. If Gary is not cold and Gary is not blue then Gary is smart. Big things are not nice. If Gary is smart then Gary is not nice.
Bob is green.
("Bob" "is" "green" "+")
Gary is big.
("Gary" "is" "big" "+")
If something is green and not blue then it is not young.
((("something" "is" "green" "+") ("something" "is" "blue" "~")) -> ("something" "is" "young" "-"))
All blue, cold things are smart.
((("something" "is" "blue" "+") ("something" "is" "cold" "+")) -> ("something" "is" "smart" "+"))
Green things are cold.
((("something" "is" "green" "+")) -> ("something" "is" "cold" "+"))
All nice things are big.
((("something" "is" "nice" "+")) -> ("something" "is" "big" "+"))
If Bob is blue and Bob is not cold then Bob is smart.
((("Bob" "is" "blue" "+") ("Bob" "is" "cold" "~")) -> ("Bob" "is" "smart" "+"))
If Gary is not cold and Gary is not blue then Gary is smart.
((("Gary" "is" "cold" "~") ("Gary" "is" "blue" "~")) -> ("Gary" "is" "smart" "+"))
Big things are not nice.
((("something" "is" "big" "+")) -> ("something" "is" "nice" "-"))
If Gary is smart then Gary is not nice.
((("Gary" "is" "smart" "+")) -> ("Gary" "is" "nice" "-"))
Gary is big.
True
1
proof
[(triple2)]
("Gary" "is" "big" "+")
triple2
Gary is not big.
False
1
inv-proof
[(triple2)]
("Gary" "is" "big" "-")
triple2
Gary is not nice.
True
2
proof
[(((triple2) -> rule7))]
("Gary" "is" "nice" "-")
((triple2) -> (rule7 % int1))
Gary is not nice.
("Gary" "is" "nice" "-")
int1
Bob is not cold.
False
2
inv-proof
[(((triple1) -> rule3))]
("Bob" "is" "cold" "-")
((triple1) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Gary is not cold.
Unknown
inv-rconc
[@1: Gary is cold.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "cold" "-")
Bob is smart.
Unknown
rconc
[@1: Bob is smart.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "smart" "+")
Bob is not blue.
Unknown
inv-random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "-")
Bob is young.
Unknown
random
[@0: Bob is young.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "young" "+")
@0: Bob is green.[(triple1)] Gary is big.[(triple2)] @1: Bob is cold.[(((triple1) -> rule3))] Gary is not nice.[(((triple2) -> rule7))]
Bob is green.
("Bob" "is" "green" "+")
triple1
Gary is big.
("Gary" "is" "big" "+")
triple2
Bob is cold.
("Bob" "is" "cold" "+")
((triple1) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Gary is not nice.
("Gary" "is" "nice" "-")
((triple2) -> (rule7 % int1))
Gary is not nice.
("Gary" "is" "nice" "-")
int1