Charlie is kind. Gary is not big. Gary is kind. If Charlie is cold and Charlie is not big then Charlie is young. Blue people are not cold. Green, blue people are cold. All green, big people are cold. Young people are kind. Cold, young people are green. Kind people are blue. If someone is young and not kind then they are not quiet.
Charlie is kind.
("Charlie" "is" "kind" "+")
Gary is not big.
("Gary" "is" "big" "-")
Gary is kind.
("Gary" "is" "kind" "+")
If Charlie is cold and Charlie is not big then Charlie is young.
((("Charlie" "is" "cold" "+") ("Charlie" "is" "big" "~")) -> ("Charlie" "is" "young" "+"))
Blue people are not cold.
((("someone" "is" "blue" "+")) -> ("someone" "is" "cold" "-"))
Green, blue people are cold.
((("someone" "is" "green" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "cold" "+"))
All green, big people are cold.
((("someone" "is" "green" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "cold" "+"))
Young people are kind.
((("someone" "is" "young" "+")) -> ("someone" "is" "kind" "+"))
Cold, young people are green.
((("someone" "is" "cold" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "green" "+"))
Kind people are blue.
((("someone" "is" "kind" "+")) -> ("someone" "is" "blue" "+"))
If someone is young and not kind then they are not quiet.
((("someone" "is" "young" "+") ("someone" "is" "kind" "~")) -> ("someone" "is" "quiet" "-"))
Gary is kind.
True
1
proof
[(triple3)]
("Gary" "is" "kind" "+")
triple3
Gary is not kind.
False
1
inv-proof
[(triple3)]
("Gary" "is" "kind" "-")
triple3
Gary is blue.
True
2
proof
[(((triple3) -> rule7))]
("Gary" "is" "blue" "+")
((triple3) -> (rule7 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Charlie is not blue.
False
2
inv-proof
[(((triple1) -> rule7))]
("Charlie" "is" "blue" "-")
((triple1) -> (rule7 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Gary is not cold.
True
3
proof
[(((((triple3) -> rule7)) -> rule2))]
("Gary" "is" "cold" "-")
((((triple3) -> (rule7 % int2))) -> (rule2 % int1))
Gary is not cold.
("Gary" "is" "cold" "-")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is cold.
False
3
inv-proof
[(((((triple3) -> rule7)) -> rule2))]
("Gary" "is" "cold" "+")
((((triple3) -> (rule7 % int2))) -> (rule2 % int1))
Gary is not cold.
("Gary" "is" "cold" "-")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is not green.
Unknown
inv-rconc
[@1: Gary is green.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Gary" "is" "green" "-")
Charlie is green.
Unknown
rconc
[@1: Charlie is green.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Charlie" "is" "green" "+")
Charlie is not young.
Unknown
inv-rconc
[@1: Charlie is young.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "young" "-")
Charlie is big.
Unknown
random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "+")
Gary is not quiet.
Unknown
inv-random
[@0: Gary is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "quiet" "-")
Charlie is quiet.
Unknown
random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "+")
@0: Charlie is kind.[(triple1)] Gary is kind.[(triple3)] Gary is not big.[(triple2)] @1: Charlie is blue.[(((triple1) -> rule7))] Gary is blue.[(((triple3) -> rule7))] @2: Charlie is not cold.[(((((triple1) -> rule7)) -> rule2))] Gary is not cold.[(((((triple3) -> rule7)) -> rule2))]
Charlie is kind.
("Charlie" "is" "kind" "+")
triple1
Gary is kind.
("Gary" "is" "kind" "+")
triple3
Gary is not big.
("Gary" "is" "big" "-")
triple2
Charlie is blue.
("Charlie" "is" "blue" "+")
((triple1) -> (rule7 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
((triple3) -> (rule7 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Charlie is not cold.
("Charlie" "is" "cold" "-")
((((triple1) -> (rule7 % int2))) -> (rule2 % int1))
Charlie is not cold.
("Charlie" "is" "cold" "-")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Gary is not cold.
("Gary" "is" "cold" "-")
((((triple3) -> (rule7 % int2))) -> (rule2 % int1))
Gary is not cold.
("Gary" "is" "cold" "-")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2