Charlie is big. Charlie is kind. Charlie is nice. Charlie is round. Charlie is young. Gary is cold. Gary is kind. If someone is big and round then they are green. All round people are cold. If someone is green then they are young. If someone is nice then they are young. If someone is round then they are young. If someone is green and round then they are big. If someone is young and kind then they are nice. All green people are nice.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is kind.
("Gary" "is" "kind" "+")
If someone is big and round then they are green.
((("someone" "is" "big" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "green" "+"))
All round people are cold.
((("someone" "is" "round" "+")) -> ("someone" "is" "cold" "+"))
If someone is green then they are young.
((("someone" "is" "green" "+")) -> ("someone" "is" "young" "+"))
If someone is nice then they are young.
((("someone" "is" "nice" "+")) -> ("someone" "is" "young" "+"))
If someone is round then they are young.
((("someone" "is" "round" "+")) -> ("someone" "is" "young" "+"))
If someone is green and round then they are big.
((("someone" "is" "green" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "big" "+"))
If someone is young and kind then they are nice.
((("someone" "is" "young" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "nice" "+"))
All green people are nice.
((("someone" "is" "green" "+")) -> ("someone" "is" "nice" "+"))
Charlie is big.
True
1
proof
[(triple1)]
("Charlie" "is" "big" "+")
triple1
Charlie is not nice.
False
1
inv-proof
[(triple3 OR ((triple5 triple2) -> rule7) OR ((((triple1 triple4) -> rule1)) -> rule8) OR ((((triple4) -> rule5) triple2) -> rule7) OR ((((((triple1 triple4) -> rule1)) -> rule3) triple2) -> rule7))]
("Charlie" "is" "nice" "-")
triple3
((triple5 triple2) -> (rule7 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
((((triple1 triple4) -> (rule1 % int2))) -> (rule8 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
((((triple4) -> (rule5 % int2)) triple2) -> (rule7 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
((((((triple1 triple4) -> (rule1 % int3))) -> (rule3 % int2)) triple2) -> (rule7 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
Charlie is cold.
True
2
proof
[(((triple4) -> rule2))]
("Charlie" "is" "cold" "+")
((triple4) -> (rule2 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is not green.
False
3
inv-proof
[(((triple1 triple4) -> rule1))]
("Charlie" "is" "green" "-")
((triple1 triple4) -> (rule1 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Gary is not nice.
Unknown
inv-rconc
[@4: Gary is nice.[CWA. Example of deepest failure = (rule7 <- rule4 <- rule8 <- rule1 <- FAIL)]]
("Gary" "is" "nice" "-")
Gary is green.
Unknown
rconc
[@1: Gary is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "green" "+")
@0: Charlie is big.[(triple1)] Charlie is kind.[(triple2)] Charlie is nice.[(triple3 OR ((triple5 triple2) -> rule7) OR ((((triple1 triple4) -> rule1)) -> rule8) OR ((((triple4) -> rule5) triple2) -> rule7) OR ((((((triple1 triple4) -> rule1)) -> rule3) triple2) -> rule7))] Charlie is round.[(triple4)] Charlie is young.[(triple5 OR ((triple3) -> rule4) OR ((triple4) -> rule5) OR ((((triple1 triple4) -> rule1)) -> rule3) OR ((((((triple1 triple4) -> rule1)) -> rule8)) -> rule4))] Gary is cold.[(triple6)] Gary is kind.[(triple7)] @1: Charlie is cold.[(((triple4) -> rule2))] Charlie is green.[(((triple1 triple4) -> rule1))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Charlie is kind.
("Charlie" "is" "kind" "+")
triple2
Charlie is nice.
("Charlie" "is" "nice" "+")
triple3
((triple5 triple2) -> (rule7 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
((((triple1 triple4) -> (rule1 % int2))) -> (rule8 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
((((triple4) -> (rule5 % int2)) triple2) -> (rule7 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
((((((triple1 triple4) -> (rule1 % int3))) -> (rule3 % int2)) triple2) -> (rule7 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
Charlie is round.
("Charlie" "is" "round" "+")
triple4
Charlie is young.
("Charlie" "is" "young" "+")
triple5
((triple3) -> (rule4 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
((triple4) -> (rule5 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
((((triple1 triple4) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
((((((triple1 triple4) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
Gary is cold.
("Gary" "is" "cold" "+")
triple6
Gary is kind.
("Gary" "is" "kind" "+")
triple7
Charlie is cold.
("Charlie" "is" "cold" "+")
((triple4) -> (rule2 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
((triple1 triple4) -> (rule1 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1