Gary is red. Gary is young. Harry is big. Harry is not cold. Harry is kind. Harry is round. Harry is young. If someone is white then they are not big. All white people are not big. All red people are not cold. White people are not cold. If Gary is red and Gary is not young then Gary is cold. If Harry is round and Harry is white then Harry is cold. Cold people are white. If someone is cold then they are round.
Gary is red.
("Gary" "is" "red" "+")
Gary is young.
("Gary" "is" "young" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is not cold.
("Harry" "is" "cold" "-")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is young.
("Harry" "is" "young" "+")
If someone is white then they are not big.
((("someone" "is" "white" "+")) -> ("someone" "is" "big" "-"))
All white people are not big.
((("someone" "is" "white" "+")) -> ("someone" "is" "big" "-"))
All red people are not cold.
((("someone" "is" "red" "+")) -> ("someone" "is" "cold" "-"))
White people are not cold.
((("someone" "is" "white" "+")) -> ("someone" "is" "cold" "-"))
If Gary is red and Gary is not young then Gary is cold.
((("Gary" "is" "red" "+") ("Gary" "is" "young" "~")) -> ("Gary" "is" "cold" "+"))
If Harry is round and Harry is white then Harry is cold.
((("Harry" "is" "round" "+") ("Harry" "is" "white" "+")) -> ("Harry" "is" "cold" "+"))
Cold people are white.
((("someone" "is" "cold" "+")) -> ("someone" "is" "white" "+"))
If someone is cold then they are round.
((("someone" "is" "cold" "+")) -> ("someone" "is" "round" "+"))
Gary is red.
True
1
proof
[(triple1)]
("Gary" "is" "red" "+")
triple1
Harry is not big.
False
1
inv-proof
[(triple3)]
("Harry" "is" "big" "-")
triple3
Gary is not cold.
True
2
proof
[(((triple1) -> rule3))]
("Gary" "is" "cold" "-")
((triple1) -> (rule3 % int1))
Gary is not cold.
("Gary" "is" "cold" "-")
int1
Gary is cold.
False
2
inv-proof
[(((triple1) -> rule3))]
("Gary" "is" "cold" "+")
((triple1) -> (rule3 % int1))
Gary is not cold.
("Gary" "is" "cold" "-")
int1
Gary is not round.
Unknown
inv-rconc
[@1: Gary is round.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Gary" "is" "round" "-")
Gary is white.
Unknown
rconc
[@1: Gary is white.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Gary" "is" "white" "+")
Gary is not kind.
Unknown
inv-random
[@0: Gary is kind.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "kind" "-")
Gary is big.
Unknown
random
[@0: Gary is big.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "big" "+")
@0: Gary is red.[(triple1)] Gary is young.[(triple2)] Harry is big.[(triple3)] Harry is kind.[(triple5)] Harry is not cold.[(triple4)] Harry is round.[(triple6)] Harry is young.[(triple7)] @1: Gary is not cold.[(((triple1) -> rule3))]
Gary is red.
("Gary" "is" "red" "+")
triple1
Gary is young.
("Gary" "is" "young" "+")
triple2
Harry is big.
("Harry" "is" "big" "+")
triple3
Harry is kind.
("Harry" "is" "kind" "+")
triple5
Harry is not cold.
("Harry" "is" "cold" "-")
triple4
Harry is round.
("Harry" "is" "round" "+")
triple6
Harry is young.
("Harry" "is" "young" "+")
triple7
Gary is not cold.
("Gary" "is" "cold" "-")
((triple1) -> (rule3 % int1))
Gary is not cold.
("Gary" "is" "cold" "-")
int1