Charlie is big. Charlie is blue. Charlie is kind. Charlie is nice. Charlie is young. Gary is blue. Gary is cold. If someone is blue and cold then they are big. If someone is blue then they are cold. If Charlie is kind and Charlie is not cold then Charlie is not big. If someone is big and not blue then they are not white. If someone is cold and not blue then they are not white. If someone is big and not nice then they are young. If someone is nice and not big then they are young. Kind, blue people are young.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is cold.
("Gary" "is" "cold" "+")
If someone is blue and cold then they are big.
((("someone" "is" "blue" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "big" "+"))
If someone is blue then they are cold.
((("someone" "is" "blue" "+")) -> ("someone" "is" "cold" "+"))
If Charlie is kind and Charlie is not cold then Charlie is not big.
((("Charlie" "is" "kind" "+") ("Charlie" "is" "cold" "~")) -> ("Charlie" "is" "big" "-"))
If someone is big and not blue then they are not white.
((("someone" "is" "big" "+") ("someone" "is" "blue" "~")) -> ("someone" "is" "white" "-"))
If someone is cold and not blue then they are not white.
((("someone" "is" "cold" "+") ("someone" "is" "blue" "~")) -> ("someone" "is" "white" "-"))
If someone is big and not nice then they are young.
((("someone" "is" "big" "+") ("someone" "is" "nice" "~")) -> ("someone" "is" "young" "+"))
If someone is nice and not big then they are young.
((("someone" "is" "nice" "+") ("someone" "is" "big" "~")) -> ("someone" "is" "young" "+"))
Kind, blue people are young.
((("someone" "is" "kind" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "young" "+"))
Charlie is kind.
True
1
proof
[(triple3)]
("Charlie" "is" "kind" "+")
triple3
Gary is not blue.
False
1
inv-proof
[(triple6)]
("Gary" "is" "blue" "-")
triple6
Gary is big.
True
3
proof
[(((triple6 triple7) -> rule1) OR ((triple6 ((triple6) -> rule2)) -> rule1))]
("Gary" "is" "big" "+")
((triple6 triple7) -> (rule1 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
((triple6 ((triple6) -> (rule2 % int2))) -> (rule1 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is not big.
False
3
inv-proof
[(((triple6 triple7) -> rule1) OR ((triple6 ((triple6) -> rule2)) -> rule1))]
("Gary" "is" "big" "-")
((triple6 triple7) -> (rule1 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
((triple6 ((triple6) -> (rule2 % int2))) -> (rule1 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is not young.
Unknown
inv-rconc
[@1: Gary is young.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Gary" "is" "young" "-")
Gary is nice.
Unknown
random
[@0: Gary is nice.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "nice" "+")
Gary is not white.
Unknown
inv-random
[@0: Gary is white.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "white" "-")
Gary is kind.
Unknown
random
[@0: Gary is kind.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "kind" "+")
@0: Charlie is big.[(triple1 OR ((triple2 ((triple2) -> rule2)) -> rule1))] Charlie is blue.[(triple2)] Charlie is kind.[(triple3)] Charlie is nice.[(triple4)] Charlie is young.[(triple5 OR ((triple3 triple2) -> rule8))] Gary is blue.[(triple6)] Gary is cold.[(triple7 OR ((triple6) -> rule2))] @1: Charlie is cold.[(((triple2) -> rule2))] Gary is big.[(((triple6 triple7) -> rule1) OR ((triple6 ((triple6) -> rule2)) -> rule1))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
((triple2 ((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
triple2
Charlie is kind.
("Charlie" "is" "kind" "+")
triple3
Charlie is nice.
("Charlie" "is" "nice" "+")
triple4
Charlie is young.
("Charlie" "is" "young" "+")
triple5
((triple3 triple2) -> (rule8 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
triple6
Gary is cold.
("Gary" "is" "cold" "+")
triple7
((triple6) -> (rule2 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
((triple2) -> (rule2 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
((triple6 triple7) -> (rule1 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
((triple6 ((triple6) -> (rule2 % int2))) -> (rule1 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2