Charlie is blue. Charlie is cold. Charlie is green. Charlie is kind. Charlie is smart. Charlie is white. Charlie is young. If someone is blue and young then they are cold. All smart, kind people are young. Smart, cold people are kind.
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Charlie is young.
("Charlie" "is" "young" "+")
If someone is blue and young then they are cold.
((("someone" "is" "blue" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "cold" "+"))
All smart, kind people are young.
((("someone" "is" "smart" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "young" "+"))
Smart, cold people are kind.
((("someone" "is" "smart" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "kind" "+"))
Charlie is white.
True
1
proof
[(triple6)]
("Charlie" "is" "white" "+")
triple6
Charlie is not cold.
False
1
inv-proof
[(triple2 OR ((triple1 triple7) -> rule1) OR ((triple1 ((triple5 triple4) -> rule2)) -> rule1))]
("Charlie" "is" "cold" "-")
triple2
((triple1 triple7) -> (rule1 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
((triple1 ((triple5 triple4) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
@0: Charlie is blue.[(triple1)] Charlie is cold.[(triple2 OR ((triple1 triple7) -> rule1) OR ((triple1 ((triple5 triple4) -> rule2)) -> rule1))] Charlie is green.[(triple3)] Charlie is kind.[(triple4 OR ((triple5 triple2) -> rule3) OR ((triple5 ((triple1 triple7) -> rule1)) -> rule3))] Charlie is smart.[(triple5)] Charlie is white.[(triple6)] Charlie is young.[(triple7 OR ((triple5 triple4) -> rule2) OR ((triple5 ((triple5 triple2) -> rule3)) -> rule2))]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
Charlie is cold.
("Charlie" "is" "cold" "+")
triple2
((triple1 triple7) -> (rule1 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
((triple1 ((triple5 triple4) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
triple3
Charlie is kind.
("Charlie" "is" "kind" "+")
triple4
((triple5 triple2) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
((triple5 ((triple1 triple7) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
triple5
Charlie is white.
("Charlie" "is" "white" "+")
triple6
Charlie is young.
("Charlie" "is" "young" "+")
triple7
((triple5 triple4) -> (rule2 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
((triple5 ((triple5 triple2) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2